English
A T0 space is equivalent to the pairwise existence, for distinct x,y, of an open set U with exactly one of x,y in U.
Русский
T0-пространство эквивалентно существованию для любых различных x,y открытого множества U, где ровно одно из x,y принадлежит U.
LaTeX
$$$T0Space X \iff Pairwise\ fun\ x\ y \Rightarrow \exists U: Set X, IsOpen U \land Xor'(x\in U)(y\in U).$$$
Lean4
theorem t0Space_iff_exists_isOpen_xor'_mem (X : Type u) [TopologicalSpace X] :
T0Space X ↔ Pairwise fun x y => ∃ U : Set X, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U) := by
simp only [t0Space_iff_not_inseparable, xor_iff_not_iff, not_forall, exists_prop, inseparable_iff_forall_isOpen,
Pairwise]