map_extend_nhds_of_boundaryless — Mathlib

English

If the chart I is boundaryless, the extended map sends neighborhoods to neighborhoods without restriction.

Русский

Если I погранично бесконечен, отображение расширения отправляет окрестности в окрестности без ограничений.

LaTeX

$$$[I.Boundaryless] \\Rightarrow map(f^{\\mathrm{extend}}_I)(\\mathcal{N}(x)) = \\mathcal{N}(f^{\\mathrm{extend}}_I(x)).$$$

Lean4

theorem map_extend_nhds_of_boundaryless [I.Boundaryless] {x : M} (hx : x ∈ f.source) :
    map (f.extend I) (𝓝 x) = 𝓝 (f.extend I x) := by rw [f.map_extend_nhds hx, I.range_eq_univ, nhdsWithin_univ]

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