English
Let f be an open partial homeomorphism between manifolds M and H, and let its extension f.extend I be considered in a chart. For any point y in the source of f, the pushforward by the extended chart maps the nhds within a subset s of y to the nhds at the image, computed inside the image of s under the extension. In symbols, the pushforward of 𝓝[s](y) by f.extend I equals 𝓝[f.extend I '' ((f.extend I).source ∩ s)](f.extend I y).
Русский
Пусть f — открытая частичная гомеморфизма между многообразиями M и H, а f.extend I — его хартова продолжение. Для любой точки y из области определения f, образованное переходом по расширенной карте отображает окрестность nhdsWithin s(y) в окрестность nhdsAt f.extend I y внутри образа s; то есть map(f.extend I)(nhdsWithin y s) = nhdsWithin((f.extend I y)) (f.extend I '' ((f.extend I).source ∩ s)).
LaTeX
$$$\\mathrm{map}\\!\\left(f^{\\mathrm{ext}}\\right)\\big(\\mathcal{N}_{s}(y)\\big) = \\mathcal{N}_{f^{\\mathrm{ext}}(y)}\\big(f^{\\mathrm{ext}}\\big[\\,(f^{\\mathrm{ext}}).source \\cap s\\,\\big]\\big)$, \\quad y \\in f.source.$$$
Lean4
theorem map_extend_nhdsWithin_eq_image {y : M} (hy : y ∈ f.source) :
map (f.extend I) (𝓝[s] y) = 𝓝[f.extend I '' ((f.extend I).source ∩ s)] f.extend I y :=
by
set e := f.extend I
calc
map e (𝓝[s] y) = map e (𝓝[e.source ∩ s] y) :=
congr_arg (map e) (nhdsWithin_inter_of_mem (extend_source_mem_nhdsWithin f hy)).symm
_ = 𝓝[e '' (e.source ∩ s)] e y :=
((f.extend I).leftInvOn.mono inter_subset_left).map_nhdsWithin_eq
((f.extend I).left_inv <| by rwa [f.extend_source]) (continuousAt_extend_symm f hy).continuousWithinAt
(continuousAt_extend f hy).continuousWithinAt
