map_extend_nhds — Mathlib

English

The image of a neighborhood under the extended chart equals a neighborhood of the image point within the target range.

Русский

Образ окрестности под расширенным чартом равен окрестности образа в области диапазона.

LaTeX

$$$ map(f^{\\mathrm{extend}}_I)(\\mathcal{N}(x)) = \\mathcal{N}_{\\mathrm{range}(I)}(f^{\\mathrm{extend}}_I(x)). $$$

Lean4

theorem map_extend_nhds {x : M} (hy : x ∈ f.source) : map (f.extend I) (𝓝 x) = 𝓝[range I] f.extend I x := by
  rwa [extend_coe, comp_apply, ← I.map_nhds_eq, ← f.map_nhds_eq, map_map]

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