English
A space is T0 iff for any two points a,b, at least one is not in the closure of the singleton of the other.
Русский
Пространство является T0 тогда и только тогда, когда для любых двух точек a и b по меньшей мере одна не принадлежит замыканию множества {b} (или {a}).
LaTeX
$$$T0Space X \\iff \\forall a,b \\in X,\ a \\notin \\overline{\\{b\\}} \\lor b \\notin \\overline{\\{a\\}}$$$
Lean4
theorem t0Space_iff_or_notMem_closure (X : Type u) [TopologicalSpace X] :
T0Space X ↔ Pairwise fun a b : X => a ∉ closure ({ b } : Set X) ∨ b ∉ closure ({ a } : Set X) := by
simp only [t0Space_iff_not_inseparable, inseparable_iff_mem_closure, not_and_or]