English
If hl gives a derivative of l at y and hy ensures y = f(x), then the derivative of l ∘ f at x is given by the same Fréchet derivative applied to the derivative of f.
Русский
Если hl задаёт производную л в точке y и hy обеспечивает равенство y = f(x), то производная композиции l ∘ f в x равна той же Фреше-деривативе, применённой к производной f.
LaTeX
$$$$HasFDerivWithinAt l l' t y \land HasDerivWithinAt f f' s x \land MapsTo f s t \land y = f x \Rightarrow HasDerivWithinAt (l \circ f) (l' f') s x$$$$
Lean4
/-- The composition `l ∘ f` where `l : F → E` and `f : 𝕜 → F`, has a derivative within a set
equal to the Fréchet derivative of `l` applied to the derivative of `f`. -/
theorem comp_hasDerivWithinAt_of_eq {t : Set F} (hl : HasFDerivWithinAt l l' t y) (hf : HasDerivWithinAt f f' s x)
(hst : MapsTo f s t) (hy : y = f x) : HasDerivWithinAt (l ∘ f) (l' f') s x := by rw [hy] at hl;
exact hl.comp_hasDerivWithinAt x hf hst
