English
If x ∈ f.source and s ⊆ f.source, then the nhdsWithin of s under the inverse extension maps to 𝓝 x through the preimage by the extended chart.
Русский
Если x ∈ f.source и s ⊆ f.source, то окрестности nhdsWithin по обратной карте отображаются через предобраз в 𝓝 x.
LaTeX
$$$s \\subseteq f.source \\Rightarrow (f^{\\mathrm{ext}})^{-1}[s] \\in 𝓝 x$$$
Lean4
/-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point
in the source is a neighborhood of the preimage, within a set. -/
theorem extend_preimage_mem_nhdsWithin {x : M} (h : x ∈ f.source) (ht : t ∈ 𝓝[s] x) :
(f.extend I).symm ⁻¹' t ∈ 𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I x := by
rwa [← map_extend_symm_nhdsWithin f (I := I) h, mem_map] at ht