isTotallyDisconnected_of_isClopen_set

English

If for all distinct x, y there exists a clopen set separating them, then the space is totally disconnected.

Русский

Если для любых различных точек существует клип-открытое разделяющее множество, то пространство полностью раздельно.

LaTeX

$$IsTotallyDisconnected s$$

Lean4

/-- Let `X` be a topological space, and suppose that for all distinct `x,y ∈ X`, there
  is some clopen set `U` such that `x ∈ U` and `y ∉ U`. Then `X` is totally disconnected. -/
@[deprecated totallySeparatedSpace_iff_exists_isClopen (since := "2025-04-03")]
theorem isTotallyDisconnected_of_isClopen_set {X : Type*} [TopologicalSpace X]
    (hX : Pairwise (∃ (U : Set X), IsClopen U ∧ · ∈ U ∧ · ∉ U)) : IsTotallyDisconnected (Set.univ : Set X) :=
  (totallySeparatedSpace_iff X).mp (totallySeparatedSpace_iff_exists_isClopen.mpr hX) |>.isTotallyDisconnected

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