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.locallyCompactSpace_of_addGroup {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (K : TopologicalSpace.PositiveCompacts G) : LocallyCompactSpace G

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

abbrev TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup.match_1 {G : Type u_1} [TopologicalSpace G] (K : TopologicalSpace.PositiveCompacts G) (motive : Set.Nonempty (interior ↑K) → Prop) : ∀ (x : Set.Nonempty (interior ↑K)), (∀ (_x : G) (hx : _x ∈ interior ↑K), motive (_ : ∃ (x : G), x ∈ interior ↑K)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

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

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

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

Equations

• (_ : ContinuousVAdd G (G ⧸ Γ)) = (_ : ContinuousVAdd G (G ⧸ Γ))

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

Equations

• (_ : ContinuousSMul G (G ⧸ Γ)) = (_ : ContinuousSMul G (G ⧸ Γ))