English
If two maps agree on s, their tangent maps within s are equal at all points of s.
Русский
Если две отображения совпадают на s, их тангентообразные отображения внутри s равны на s.
LaTeX
$$$\\forall p\\in TM,\\; p.1\\in s\\land (f=f_1\\text{ on }s)\\Rightarrow tangentMapWithin I I' f\\,s\\,p = tangentMapWithin I I' f_1\\,s\\,p$$$
Lean4
theorem comp (hg : HasMFDerivWithinAt I' I'' g u (f x) g') (hf : HasMFDerivWithinAt I I' f s x f') (hst : s ⊆ f ⁻¹' u) :
HasMFDerivWithinAt I I'' (g ∘ f) s x (g'.comp f') :=
by
refine ⟨ContinuousWithinAt.comp hg.1 hf.1 hst, ?_⟩
have A :
HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f)
(ContinuousLinearMap.comp g' f' : E →L[𝕜] E'') ((extChartAt I x).symm ⁻¹' s ∩ range I) ((extChartAt I x) x) :=
by
have :
(extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' (f x)).source) ∈
𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x :=
extChartAt_preimage_mem_nhdsWithin (hf.1.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds _))
unfold HasMFDerivWithinAt at *
rw [← hasFDerivWithinAt_inter' this, ← extChartAt_preimage_inter_eq] at hf ⊢
have : writtenInExtChartAt I I' x f ((extChartAt I x) x) = (extChartAt I' (f x)) (f x) := by simp only [mfld_simps]
rw [← this] at hg
apply HasFDerivWithinAt.comp ((extChartAt I x) x) hg.2 hf.2 _
intro y hy
simp only [mfld_simps] at hy
have : f (((chartAt H x).symm : H → M) (I.symm y)) ∈ u := hst hy.1.1
simp only [hy, this, mfld_simps]
apply A.congr_of_eventuallyEq (writtenInExtChartAt_comp hf.1)
simp only [mfld_simps]
