t2Space — Mathlib

English

In a T25 space, the space is Hausdorff (T2): any two distinct points have disjoint neighborhoods.

Русский

В T25-пространстве пространство является хаусдорфовым (T2): любые две различные точки имеют непересекающиеся окрестности.

LaTeX

$$$\forall x,y:\; x \neq y \Rightarrow \exists U,V:\; x\in U,\ y\in V,\ U\cap V = \varnothing.$$$

Lean4

instance (priority := 100) t2Space [T25Space X] : T2Space X :=
  t2Space_iff_disjoint_nhds.2 fun _ _ hne =>
    (disjoint_lift'_closure_nhds.2 hne).mono (le_lift'_closure _) (le_lift'_closure _)

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