English
If y ∈ (extChartAt I x).source, then the image of nhds y under extChartAt I x equals nhds within range I at extChartAt I x y.
Русский
Если y ∈ source extChartAt I x, то образ nhds y через extChartAt I x равен nhdsWithin (range I) на extChartAt I x y.
LaTeX
$$$ map (\\mathrm{extChartAt} I x) (\\mathcal{N} y) = \\mathcal{N}_{\\mathrm{range} I}(\\mathrm{extChartAt} I x y)$$$
Lean4
theorem map_extChartAt_nhds' {x y : M} (hy : y ∈ (extChartAt I x).source) :
map (extChartAt I x) (𝓝 y) = 𝓝[range I] extChartAt I x y :=
map_extend_nhds _ <| by rwa [← extChartAt_source I]