English
If g' is differentiable within u at y', g is differentiable within t at y, f is differentiable within s at x, and y = g(y) = y', with corresponding maps, then the derivative of the triple composition g' ∘ g ∘ f is the composition of derivatives in the expected order: fderivWithin g' ∘ g ∘ f at x equals fderivWithin g' at y' composed with (fderivWithin g at y composed with fderivWithin f at x).
Русский
Если g' дифференцируется внутри u в y', g дифференцируется внутри t в y, f дифференцируется внутри s в x, и выполняются совместимые равенства, то производная от композиции g' ∘ g ∘ f равна композиции соответствующих производных: fderivWithin g'∘g∘f = fderivWithin g' ∘ (fderivWithin g ∘ f).
LaTeX
$$$$ fderivWithin_{\mathbb{K}}(g' \circ g \circ f)\, s\, x = \big( fderivWithin_{\mathbb{K}} g'\, u\, y' \big) \circ \Big( \big( fderivWithin_{\mathbb{K}} g\, t\, y \big) \circ \big( fderivWithin_{\mathbb{K}} f\, s\, x \big) \Big). $$$$
Lean4
/-- Ternary version of `fderivWithin_comp`, with equality assumptions of basepoints added, in
order to apply more easily as a rewrite from right-to-left. -/
theorem fderivWithin_comp₃ {g' : G → G'} {g : F → G} {t : Set F} {u : Set G} {y : F} {y' : G}
(hg' : DifferentiableWithinAt 𝕜 g' u y') (hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x)
(h2g : MapsTo g t u) (h2f : MapsTo f s t) (h3g : g y = y') (h3f : f x = y) (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (g' ∘ g ∘ f) s x =
(fderivWithin 𝕜 g' u y').comp ((fderivWithin 𝕜 g t y).comp (fderivWithin 𝕜 f s x)) :=
by
substs h3g h3f
exact
(hg'.hasFDerivWithinAt.comp x (hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h2f) <| h2g.comp h2f).fderivWithin
hxs
