interior_singleton — Mathlib

English

If x is not isolated, then the interior of {x} is empty.

Русский

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

LaTeX

$$$\operatorname{Int} \{x\} = \emptyset$$$

Lean4

/-- If `x` is not an isolated point of a topological space, then the interior of `{x}` is empty. -/
@[simp]
theorem interior_singleton (x : X) [NeBot (𝓝[≠] x)] : interior { x } = (∅ : Set X) :=
  interior_eq_empty_iff_dense_compl.2 (dense_compl_singleton x)

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