t0Space_iff_or_notMem_closure — Mathlib

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]

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