English
For a map f between manifolds, the nhdsWithin around extChartAt x, when pulled back through extChartAt, coincides with the nhdsWithin around extChartAt x in the target using the intersection with the chart range.
Русский
Для отображения между многообразиями однородные окрестности через extChartAt совпадают после вытягивания назад через extChartAt с пересечением диапазона карты.
LaTeX
$$$\nhdsWithin((extChartAt I x).toFun x)(\mathrm{Set}) = \nhdsWithin(\mathrm{extChartAt I x}.toFun x)(\mathrm{Set}.inter(\dots)).$$$
Lean4
theorem nhdsWithin_extChartAt_symm_preimage_inter_range {f : M → M'} {x : M} (hc : ContinuousWithinAt f s x) :
𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x x) =
𝓝[(extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)]
(extChartAt I x x) :=
by
rw [← (extChartAt I x).image_source_inter_eq', ← map_extChartAt_nhdsWithin_eq_image, ← map_extChartAt_nhdsWithin,
nhdsWithin_inter_of_mem']
exact hc (extChartAt_source_mem_nhds _)
