t0Space_iff_exists_isOpen_xor'_mem

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]

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