dense_compl_singleton — Mathlib

English

If x is not isolated, then the complement of {x} is dense in the space.

Русский

Если точка x не изолирована, то комплемент множества {x} плотен во всем пространстве.

LaTeX

$$$\text{If } x \text{ is not isolated, then } (\{x\})^{c} \text{ is dense in the space}$$$

Lean4

/-- If `x` is not an isolated point of a topological space, then `{x}ᶜ` is dense in the whole
space. -/
theorem dense_compl_singleton (x : X) [NeBot (𝓝[≠] x)] : Dense ({ x }ᶜ : Set X) :=
  by
  intro y
  rcases eq_or_ne y x with (rfl | hne)
  · rwa [mem_closure_iff_nhdsWithin_neBot]
  · exact subset_closure hne

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