fderivWithin_comp' — Mathlib

English

Variant of fderivWithin_comp' specialized to the bilinear setting with bilinear operator B.

Русский

Вариант fderivWithin_comp' в билинейном контексте с билинейной операцией B.

LaTeX

$$$fderivWithin 𝕜 (y \mapsto B(f(y), g(y))) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)$$$

Lean4

/-- A variant for the derivative of a composition, written without `∘`. -/
theorem fderivWithin_comp' {g : F → G} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x))
    (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun y ↦ g (f y)) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x) :=
  fderivWithin_comp _ hg hf h hxs

Похожие утверждения