English
Let g: F → G be differentiable within t at y and f: E → F be differentiable within s at x. If f maps s into t and x is a uniquely differentiable point within s, with f(x) = y, then the derivative (within s) of the composite g ∘ f at x equals the derivative (within t) of g at y, composed with the derivative (within s) of f at x.
Русский
Пусть g: F → G дифференцируем в точке y внутри множества t, а f: E → F дифференцируем внутри s в точке x. Пусть отображение f сохраняет область: MapsTo f s t, и x является точкой с уникальной дифференцируемостью внутри s, причем f(x) = y. Тогда производная внутри s от композиции g ∘ f в точке x равна производной внутри t от g в точке f(x), примененной к производной внутри s от f в точке x.
LaTeX
$$$$ \\operatorname{fderivWithin}_{\\mathbb{K}}(\\lambda y. g(f(y)))\\,s\\,x = \\big( \\operatorname{fderivWithin}_{\\mathbb{K}}\, g\\,t\\,(f(x)) \\big) \\circ \\operatorname{fderivWithin}_{\\mathbb{K}}\, f\\,s\\,x. $$$$
Lean4
/-- A variant for the derivative of a composition, written without `∘`. -/
theorem fderivWithin_comp_of_eq' {g : F → G} {t : Set F} {y : F} (hg : DifferentiableWithinAt 𝕜 g t y)
(hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) :
fderivWithin 𝕜 (fun y ↦ g (f y)) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x) := by subst hy;
exact fderivWithin_comp _ hg hf h hxs
