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 ⧸ Γ)