TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup
theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalAddGroup G],
TopologicalSpace.PositiveCompacts G → LocallyCompactSpace G
This theorem states that for every topological additive group G, if there exists a compact set with a nonempty interior in G (expressed as `TopologicalSpace.PositiveCompacts G`), then G is a locally compact space (`LocallyCompactSpace G`). In other words, in the context of topological additive groups, the existence of a compact set with nonempty interior implies local compactness.
More concisely: In the context of topological additive groups, the presence of a compact set with nonempty interior implies local compactness.
|
TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group
theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group :
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : TopologicalGroup G],
TopologicalSpace.PositiveCompacts G → LocallyCompactSpace G
This theorem states that for any type `G` that is a topological space, a group, and a topological group, if there exists a positive compact - a compact set with nonempty interior - then `G` is a locally compact space. A locally compact space is a topological space in which every point has a local base of compact neighborhoods. This theorem essentially connects the concepts of topological groups and locally compact spaces, leveraging the existence of a positive compact.
More concisely: A topological space that is a group and a topological group with a positive compact element is locally compact.
|