English
If y lies in the source of f and s is a subset of that source, then the image under the extended chart maps the nhds of y restricted to s to the nhds at the image of s under the extension. Equivalently, map (f.extend I) (nhdsWithin y s) = nhdsWithin (f.extend I y) (f.extend I '' s).
Русский
Пусть y принадлежит области определения f, и s ⊆ f.source. Тогда образование окрестности nhdsWithin на s перейдет через продолжение карты в окрестности nhdsWithin изображения s под продолжением.
LaTeX
$$$\\mathrm{map}\\!\\left(f^{\\mathrm{ext}}\\right)(\\mathcal{N}_{s}(y)) = \\mathcal{N}_{f^{\\mathrm{ext}}(y)}\\big(f^{\\mathrm{ext}}[s]\\big)$, при условии $y \\in f.source$ и $s \\subseteq f.source$.$$
Lean4
theorem map_extend_nhdsWithin_eq_image_of_subset {y : M} (hy : y ∈ f.source) (hs : s ⊆ f.source) :
map (f.extend I) (𝓝[s] y) = 𝓝[f.extend I '' s] f.extend I y :=
by
rw [map_extend_nhdsWithin_eq_image _ hy, inter_eq_self_of_subset_right]
rwa [extend_source]
