exists_isOpen_xor'_mem — Mathlib

English

If x ≠ y in a T0 space, there exists an open set U containing exactly one of x,y.

Русский

Если x ≠ y в T0-пространстве, существует открытое множество U, содержащее ровно одну из точек x,y.

LaTeX

$$$x \neq y \Rightarrow ∃ U, IsOpen(U) ∧ Xor'(x ∈ U)(y ∈ U).$$$

Lean4

theorem exists_isOpen_xor'_mem [T0Space X] {x y : X} (h : x ≠ y) : ∃ U : Set X, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U) :=
  (t0Space_iff_exists_isOpen_xor'_mem X).1 ‹_› h

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