t1Space_iff_specializes_imp_eq — Mathlib

English

For any X with a T1 space structure, the specialization relation is a function that yields equality; equivalently the specialization relation is equal to equality.

Русский

Для T1-пространства специализация совпадает с равенством точек.

LaTeX

$$specializes_iff_eq in T1Space X gives (· ⤳ ·) = @Eq X.$$

Lean4

theorem t1Space_iff_specializes_imp_eq : T1Space X ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y :=
  (t1Space_TFAE X).out 0 9

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