lift'_nhds_interior — Mathlib

English

Lifting the basis through interior preserves the neighborhood filter; interior refinement yields the same neighborhoods.

Русский

Поднятие базы через interior сохраняет фильтр окрестностей; уточнение через interior дает те же окрестности.

LaTeX

$$$(\\mathcal N(x)).lift'\\mathrm{interior} = \\mathcal N(x)$$$

Lean4

@[simp]
theorem lift'_nhds_interior (x : X) : (𝓝 x).lift' interior = 𝓝 x :=
  (nhds_basis_opens x).lift'_interior_eq_self fun _ ↦ And.right

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