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.

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 : (interior K).NonemptyProp) :
∀ (x : (interior K).Nonempty), (∀ (_x : G) (hx : _x interior K), motive )motive x
Equations
  • =
Instances For

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