nhdsWithin_compl_singleton_le — Mathlib

English

In any T1 space, for distinct x,y, the neighborhood filter of x restricted to the complement of {x} is contained in the neighborhood filter restricted to the complement of {y}.

Русский

Для любого T1-пространства, при x ≠ y, фильтр окрестностей x внутри дополнения к {x} вложен в фильтр окрестностей x внутри дополнения к {y}.

LaTeX

$$$\\forall X [\\mathcal{T}_1(X)], \\forall x,y\\in X, x\\neq y \\Rightarrow nhdsWithin(x, X\\setminus\\{x\\}) \\le nhdsWithin(x, X\\setminus\\{y\\}).$$$

Lean4

theorem nhdsWithin_compl_singleton_le [T1Space X] (x y : X) : 𝓝[{ x }ᶜ] x ≤ 𝓝[{ y }ᶜ] x :=
  by
  rcases eq_or_ne x y with rfl | hy
  · exact Eq.le rfl
  · rw [Ne.nhdsWithin_compl_singleton hy]
    exact nhdsWithin_le_nhds

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