Theorems · Theorem · Lie groups

ProfiniteGrp.closedSubgroup_eq_sInf_open

∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] (H : ClosedSubgroup G), ↑H = sInf {N | IsOpen ↑N ∧ ↑H ≤ N}

Any closed subgroup of a profinite group is the intersection of the open subgroups containing it. See https://math.stackexchange.com/questions/5023433/closed-subgroups-of-a-compact-topological-group.

Defined in

Mathlib.Topology.Algebra.ClopenNhdofOne

Cited by

0 results in Mathlib

Foundations

Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupTopologicalSpaceIsTopologicalGroupCompactSpaceTotallyDisconnectedSpace