nhds_interior — Mathlib

English

If 𝓝 x has a basis p s, then 𝓝 x has a basis p (interior ∘ s).

Русский

Если 𝓝 x имеет базис p s, то 𝓝 x имеет базис p ( interior ∘ s ).

LaTeX

$$$ (\\mathcal N(x)).HasBasis\\, p\\, s \\Rightarrow (\\mathcal N(x)).HasBasis\\, p\\, (\\lambda i. \\operatorname{interior}(s(i))) $$$

Lean4

theorem nhds_interior {x : X} {p : ι → Prop} {s : ι → Set X} (h : (𝓝 x).HasBasis p s) :
    (𝓝 x).HasBasis p (interior <| s ·) :=
  lift'_nhds_interior x ▸ h.lift'_interior

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