closure_compl_singleton — Mathlib

English

If x is not isolated, the closure of {x}ᶜ is the whole space.

Русский

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

LaTeX

$$$\overline{\{x\}^c} = \text{univ}$$$

Lean4

/-- If `x` is not an isolated point of a topological space, then the closure of `{x}ᶜ` is the whole
space. -/
theorem closure_compl_singleton (x : X) [NeBot (𝓝[≠] x)] : closure { x }ᶜ = (univ : Set X) :=
  (dense_compl_singleton x).closure_eq

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