t1Space_iff_exists_open — Mathlib

English

A space is T1 iff for every pair of distinct points x,y there exists an open set U with x ∈ U and y ∉ U.

Русский

Т1-пространство эквивалентно тому, что для каждой пары различных точек x,y существует открытое множество U с x ∈ U и y ∉ U.

LaTeX

$$$T1Space(X) \\iff \\text{Pairwise }(\\exists U, IsOpen(U) \\land x \\in U \\land y \\notin U).$$$

Lean4

theorem t1Space_iff_exists_open : T1Space X ↔ Pairwise fun x y => ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ y ∉ U :=
  (t1Space_TFAE X).out 0 6

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