English
For a point y in the source of f, the nhds of y relative to a subset s, pushed forward by the extended chart f.extend I, equals the nhds of the image point f.extend I y relative to the image of s under the extension. This expresses the compatibility of nhdsWithin with chart extension.
Русский
Для точки y из области определения f окрестности nhdsWithin относительно s переходят через расширенную карту как окрестности nhdsWithin в точке f.extend I y относительно образа 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)$, где $ (f^{\\mathrm{ext}}).s = f^{\\mathrm{ext}}[s] $.$$
Lean4
theorem map_extend_nhdsWithin {y : M} (hy : y ∈ f.source) :
map (f.extend I) (𝓝[s] y) = 𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I y := by
rw [map_extend_nhdsWithin_eq_image f hy, nhdsWithin_inter, ← nhdsWithin_extend_target_eq _ hy, ← nhdsWithin_inter,
(f.extend I).image_source_inter_eq', inter_comm]
