t25Space — Mathlib

English

Every T3-space is a T25-space.

Русский

Каждое T3-пространство является T25-пространством.

LaTeX

$$$T3Space\; X \Rightarrow T25Space\; X.$$$

Lean4

instance (priority := 100) t25Space [T3Space X] : T25Space X :=
  by
  refine ⟨fun x y hne => ?_⟩
  rw [lift'_nhds_closure, lift'_nhds_closure]
  have : x ∉ closure { y } ∨ y ∉ closure { x } := (t0Space_iff_or_notMem_closure X).mp inferInstance hne
  simp only [← disjoint_nhds_nhdsSet, nhdsSet_singleton] at this
  exact this.elim id fun h => h.symm

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