nhdsWithin_compl_singleton — Mathlib

English

In a T1 space, for x ≠ y, the nhdsWithin of x with respect to the complement of {y} equals nhds x.

Русский

В T1-пространстве для x ≠ y окружение x внутри множества, исключающего {y}, равно обычному окружению x.

LaTeX

$$$\\nhdsWithin(x, {y}^{c}) = \\nhds(x) \\quad \\text{if } x \\neq y$$$

Lean4

theorem nhdsWithin_compl_singleton [T1Space X] {x y : X} (h : x ≠ y) : 𝓝[{ y }ᶜ] x = 𝓝 x :=
  isOpen_ne.nhdsWithin_eq h

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