comp_hasDerivWithinAt — Mathlib

English

Given hl with l' at y, hf with f' at x, and hy: y = f(x), the derivative of l ∘ f at x is l' f' as a derivative within s.

Русский

Если есть hf, hl и hy: y = f(x), то производная композиции равна l' f' внутри s.

LaTeX

$$$$HasFDerivWithinAt l l' y \land HasDerivWithinAt f f' x \land hy : y = f x \Rightarrow HasDerivWithinAt (l \circ f) (l' f') x$$$$

Lean4

theorem comp_hasDerivWithinAt (hl : HasFDerivAt l l' (f x)) (hf : HasDerivWithinAt f f' s x) :
    HasDerivWithinAt (l ∘ f) (l' f') s x :=
  hl.hasFDerivWithinAt.comp_hasDerivWithinAt x hf (mapsTo_univ _ _)

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