map_extend_nhds_of_mem_interior_range

English

The target under extended chart sits inside nhdsWithin range I around the image.

Русский

Целое под расширенным чартом лежит внутри nhdsWithin по диапазону I вокруг образа.

LaTeX

$$$ (f^{\\mathrm{extend}}_I).\\mathrm{target} \\in \\mathcal{N}_{[\\mathrm{range}(I)]}(f^{\\mathrm{extend}}_I(y)). $$$

Lean4

theorem map_extend_nhds_of_mem_interior_range {x : M} (hx : x ∈ f.source) (h'x : f.extend I x ∈ interior (range I)) :
    map (f.extend I) (𝓝 x) = 𝓝 (f.extend I x) :=
  by
  rw [f.map_extend_nhds hx, nhdsWithin_eq_nhds]
  exact mem_of_superset (isOpen_interior.mem_nhds h'x) interior_subset

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