diff_singleton — Mathlib

English

If s is dense in a T1 space and x has a nonempty punctured neighborhood, then s without x is still dense.

Русский

Если s плотно в T1-пространстве и у x существует непустое дырчатое окрестности, то s без x снова плотно.

LaTeX

$$$\text{Dense}(s) \implies \text{Dense}(s \setminus \{x\})$ under the hypothesis that 𝓝[\neq] x is nonempty.$$

Lean4

/-- Removing a non-isolated point from a dense set, one still obtains a dense set. -/
theorem diff_singleton [T1Space X] {s : Set X} (hs : Dense s) (x : X) [NeBot (𝓝[≠] x)] : Dense (s \ { x }) :=
  hs.inter_of_isOpen_right (dense_compl_singleton x) isOpen_compl_singleton

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