English
A space α is T0 if and only if there exists a pairwise separation property expressed by a uniformity basis: x ≠ y implies there exists an i with p(i) such that (x, y) ∉ s(i).
Русский
Пусть α - пространство, для которого существует базис равномерности: x ≠ y тогда существует i, такое что p(i) и (x,y) ∉ s(i).
LaTeX
$$$T0Space(\alpha) \iff \text{Pairwise} \; (x,y) => \exists i, p(i) \land (x,y) \notin s(i)$$$
Lean4
theorem t0Space_iff_uniformity' : T0Space α ↔ Pairwise fun x y ↦ ∃ r ∈ 𝓤 α, (x, y) ∉ r := by
simp [t0Space_iff_not_inseparable, inseparable_iff_ker_uniformity]