English
A variant of the chain rule for derivatives within sets, giving a compatible equality that holds for all directions v: fderivWithin g t y applied to fderivWithin f s x applied to v equals fderivWithin (g ∘ f) s x applied to v.
Русский
Вариант цепного правила внутри множеств: для всех направлений v выполняется равенство 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
/-- A version of `fderivWithin_comp` that is useful to rewrite the composition of two derivatives
into a single derivative. This version always applies, but creates a new side-goal `f x = y`. -/
theorem fderivWithin_fderivWithin {g : F → G} {f : E → F} {x : E} {y : F} {s : Set E} {t : Set F}
(hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t)
(hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) (v : E) :
fderivWithin 𝕜 g t y (fderivWithin 𝕜 f s x v) = fderivWithin 𝕜 (g ∘ f) s x v :=
by
subst y
rw [fderivWithin_comp x hg hf h hxs, coe_comp', Function.comp_apply]
