English
For any x, the preimage under extChartAt I x of a neighborhood of x within the chart’s domain is a neighborhood of x in M, when intersected with the chart range.
Русский
Для любого x предобраз под extChartAt I x окрестности x внутри области карты является окрестностью x в M, при пересечении с диапазоном карты.
LaTeX
$$$x \in M \Rightarrow (\mathrm{extChartAt} I x)^{-1} (\mathcal{N}_{\mathrm{range}(I)}(\mathrm{extChartAt} I x x)) \in 𝓝(x).$$$
Lean4
/-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of the
base point is a neighborhood of the preimage, within a set. -/
theorem extChartAt_preimage_mem_nhdsWithin {x : M} (ht : t ∈ 𝓝[s] x) :
(extChartAt I x).symm ⁻¹' t ∈ 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x :=
extChartAt_preimage_mem_nhdsWithin' (mem_extChartAt_source x) ht
