English
If a space is T0 and has a clopen basis, then it is totally separated.
Русский
Если пространство T0 и имеет базис из клипоновых множеств, то оно полностью раздельно.
LaTeX
$$$\\text{If } X \\text{ is T0 and } \\{\\text{IsClopen}\\text{ sets is a basis} \\}, \\text{ then } X \\text{ is TotallySeparated}$.$$
Lean4
/-- A T0 space with a clopen basis is totally separated. -/
theorem totallySeparatedSpace_of_t0_of_basis_clopen [T0Space X] (h : IsTopologicalBasis {s : Set X | IsClopen s}) :
TotallySeparatedSpace X := by
constructor
rintro x - y - hxy
choose U hU using exists_isOpen_xor'_mem hxy
obtain ⟨hU₀, hU₁⟩ := hU
rcases hU₁ with hx | hy
· choose V hV using h.isOpen_iff.mp hU₀ x hx.1
exact
⟨V, Vᶜ, hV.1.isOpen, hV.1.compl.isOpen, hV.2.1, notMem_subset hV.2.2 hx.2, (union_compl_self V).superset,
disjoint_compl_right⟩
· choose V hV using h.isOpen_iff.mp hU₀ y hy.1
exact
⟨Vᶜ, V, hV.1.compl.isOpen, hV.1.isOpen, notMem_subset hV.2.2 hy.2, hV.2.1,
(union_comm _ _ ▸ union_compl_self V).superset, disjoint_compl_left⟩
