English
If x' lies in the source of extChartAt I x and t is a neighborhood of x' within s, then the preimage under extChartAt I x of t is a neighborhood of extChartAt I x x' inside the preimage of s.
Русский
Если x' принадлежит источнику extChartAt I x и t окрестность x' внутри s, то предобраз под extChartAt I x окрестность t является окрестностью extChartAt I x x' внутри предобраза s.
LaTeX
$$$x' \in (extChartAt I x).source \Rightarrow (extChartAt I x)^{-1} t \in 𝓝[(extChartAt I x)^{-1} s} (extChartAt I x x').$$$
Lean4
/-- Technical lemma to rewrite suitably the preimage of an intersection under an extended chart, to
bring it into a convenient form to apply derivative lemmas. -/
theorem extChartAt_preimage_inter_eq (x : M) :
(extChartAt I x).symm ⁻¹' (s ∩ t) ∩ range I = (extChartAt I x).symm ⁻¹' s ∩ range I ∩ (extChartAt I x).symm ⁻¹' t :=
by mfld_set_tac
