# Additional results on topological groups #

A result on topological groups that has been separated out as it requires more substantial imports developing positive compacts.

theorem
TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group
{G : Type u}
[TopologicalSpace G]
[Group G]
[TopologicalGroup G]
(K : TopologicalSpace.PositiveCompacts G)
:

Every topological group in which there exists a compact set with nonempty interior is locally compact.

theorem
TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup
{G : Type u}
[TopologicalSpace G]
[AddGroup G]
[TopologicalAddGroup G]
(K : TopologicalSpace.PositiveCompacts G)
:

Every topological additive group in which there exists a compact set with nonempty interior is locally compact.