English
A ternary version of the derivative of a composition with equality assumptions, showing that for all v ∈ E, fderivWithin g t y ( fderivWithin f s x v ) equals fderivWithin (g ∘ f) s x v.
Русский
Трёхступенная версия производной композиции с равенствами базовых точек: для каждого v∈E выполняется fderivWithin g t y ( fderivWithin f s x v ) = fderivWithin (g ∘ f) s x v.
LaTeX
$$$$ \\forall v,\\; fderivWithin_{\\mathbb{K}}\, g\\, t\\, y\\big( fderivWithin_{\\mathbb{K}}\, f\\, s\\, x\\, v \\big) = fderivWithin_{\\mathbb{K}}\, (g \\circ f)\\, s\\, x\\, v. $$$$
Lean4
theorem fderiv_comp_fderivWithin {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableWithinAt 𝕜 f s x)
(hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (g ∘ f) s x = (fderiv 𝕜 g (f x)).comp (fderivWithin 𝕜 f s x) :=
(hg.hasFDerivAt.comp_hasFDerivWithinAt x hf.hasFDerivWithinAt).fderivWithin hxs
