English
If hl has a Fréchet derivative l' on t at f(x), hf has a (classical) derivative f' within s at x, and f maps s into t, then the composition l ∘ f has a derivative within s at x with derivative l' f'.
Русский
Если у hl есть Фреше-дериватив на t в точке f(x), hf — производная f внутри s в x, и f отправляет s в t, то композиция l∘f имеет внутри s производную l' f'.
LaTeX
$$$$HasFDerivWithinAt l l' t (f x) \land HasDerivWithinAt f f' s x \land MapsTo f s t \Rightarrow HasDerivWithinAt (l \circ f) (l' f') s x$$$$
Lean4
theorem comp_hasDerivAt {t : Set F} (hl : HasFDerivWithinAt l l' t (f x)) (hf : HasDerivAt f f' x)
(ht : ∀ᶠ x' in 𝓝 x, f x' ∈ t) : HasDerivAt (l ∘ f) (l' f') x := by
simpa only [one_apply, one_smul, smulRight_apply, coe_comp', (· ∘ ·)] using
(hl.comp_hasFDerivAt x hf.hasFDerivAt ht).hasDerivAt
