# Additional results on topological groups #

Two results on topological groups that have been separated out as they require more substantial imports developing either positive compacts or the compact open topology.

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

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

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

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

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

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

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

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

theorem
QuotientAddGroup.continuousVAdd.proof_1
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[TopologicalAddGroup G]
{Γ : AddSubgroup G}
[LocallyCompactSpace G]
:

ContinuousVAdd G (G ⧸ Γ)

instance
QuotientAddGroup.continuousVAdd
{G : Type w}
[AddGroup G]
[TopologicalSpace G]
[TopologicalAddGroup G]
{Γ : AddSubgroup G}
[LocallyCompactSpace G]
:

ContinuousVAdd G (G ⧸ Γ)

instance
QuotientGroup.continuousSMul
{G : Type w}
[Group G]
[TopologicalSpace G]
[TopologicalGroup G]
{Γ : Subgroup G}
[LocallyCompactSpace G]
:

ContinuousSMul G (G ⧸ Γ)