Theorems · Theorem · general topology

compact_exists_isClopen_in_isOpen

∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] {x : X}
  {U : Set X}, IsOpen U → x ∈ U → ∃ V, IsClopen V ∧ x ∈ V ∧ V ⊆ U

Every member of an open set in a compact Hausdorff totally disconnected space is contained in a clopen set contained in the open set.

Defined in

Mathlib.Topology.Separation.Profinite

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2SpaceCompactSpaceTotallyDisconnectedSpace