t0Space_iff_not_inseparable — Mathlib

English

Let X be a topological space. Then X is T0 if and only if for any two distinct points x and y in X, there exists an open set that contains exactly one of them.

Русский

Пусть X — топологическое пространство. Тогда X является T0, эквивалентно тому, что для любых двух различных точек x и y в X существует открытое множество, содержащее ровно одну из них.

LaTeX

$$$T0Space(X) \iff \forall x \neq y,\, \exists U \subseteq X, \ IsOpen(U) \land \bigl((x \in U) \land (y \notin U) \lor (x \notin U) \land (y \in U)\bigr).$$$

Lean4

theorem t0Space_iff_not_inseparable (X : Type u) [TopologicalSpace X] :
    T0Space X ↔ Pairwise fun x y : X => ¬Inseparable x y := by
  simp only [t0Space_iff_inseparable, Ne, not_imp_not, Pairwise]

Похожие утверждения