Documentation

Mathlib.Topology.Algebra.Group.Compact

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.

source
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.

source
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 ⋯) → motive x
Equations
  • ⋯ = ⋯
Instances For
    source
    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.

    source
    instance QuotientAddGroup.continuousVAdd {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {Γ : AddSubgroup G} [LocallyCompactSpace G] :
    ContinuousVAdd G (G ⧸ Γ)
    Equations
    • ⋯ = ⋯
    source
    instance QuotientGroup.continuousSMul {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] {Γ : Subgroup G} [LocallyCompactSpace G] :
    ContinuousSMul G (G ⧸ Γ)
    Equations
    • ⋯ = ⋯