interior_eq_nhds — Mathlib

English

Let X be a topological space and s ⊆ X. The interior of s is the set of all x such that the neighborhood filter at x is below the principal filter generated by s, i.e., 𝓝(x) ≤ 𝓟(s).

Русский

Пусть X — топологическое пространство и s ⊆ X. Внутренность s состоит из всех точек x, для которых 𝓝(x) ≤ 𝓟(s).

LaTeX

$$$\\operatorname{int}(s) = \\{x \\in X \\mid \\mathcal{N}(x) \\le \\mathcal{P}(s)\\}$$$

Lean4

theorem interior_eq_nhds : interior s = {x | 𝓝 x ≤ 𝓟 s} :=
  interior_eq_nhds'.trans <| by simp only [le_principal_iff]

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