English
A space is totally separated iff there exists, pairwise, a clopen cover with separating points.
Русский
Пространство полностью разделимо тогда и только тогда, когда существует попарно такой клипоновый разрез, отделяющий точки.
LaTeX
$$$TotallySeparatedSpace(\alpha) \iff Pairwise (\\exists U: Set α, IsClopen U ∧ \\cdot ∈ U ∧ \\cdot ∈ U^c)$$$
Lean4
theorem totallySeparatedSpace_iff_exists_isClopen {α : Type*} [TopologicalSpace α] :
TotallySeparatedSpace α ↔ Pairwise (∃ U : Set α, IsClopen U ∧ · ∈ U ∧ · ∈ Uᶜ) :=
by
simp only [totallySeparatedSpace_iff, IsTotallySeparated, Set.Pairwise, mem_univ, true_implies]
refine forall₃_congr fun x y _ ↦ ⟨fun ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ ↦ ?_, fun ⟨U, hU, Ux, Ucy⟩ ↦ ?_⟩
· exact ⟨U, isClopen_of_disjoint_cover_open f hU hV disj, Ux, fun Uy ↦ Set.disjoint_iff.mp disj ⟨Uy, Vy⟩⟩
· exact ⟨U, Uᶜ, hU.2, hU.compl.2, Ux, Ucy, (Set.union_compl_self U).ge, disjoint_compl_right⟩
