compact_exists_isClopen_in_isOpen

English

In a locally compact Hausdorff space, totally disconnected is equivalent to totally separated.

Русский

В локально компактном хаусдорфовом пространстве полностью несвязность эквивалентна полной раздельности.

LaTeX

$$$\\text{TotallyDisconnectedSpace } H \\iff \\text{TotallySeparatedSpace } H$ for locally compact Hausdorff $H$.$$

Lean4

/-- Every member of an open set in a compact Hausdorff totally disconnected space
  is contained in a clopen set contained in the open set. -/
theorem compact_exists_isClopen_in_isOpen {x : X} {U : Set X} (is_open : IsOpen U) (memU : x ∈ U) :
    ∃ V : Set X, IsClopen V ∧ x ∈ V ∧ V ⊆ U :=
  isTopologicalBasis_isClopen.mem_nhds_iff.1 (is_open.mem_nhds memU)

Похожие утверждения