comp_hasDerivWithinAt_of_eq — Mathlib

English

Under hl with y, hf for f, and hy: y = f(x), the derivative of l ∘ f at x is given by l' f' within s.

Русский

При hl с y, hf для f и hy: y = f(x) производная l∘f в x равна l' f' внутри s.

LaTeX

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

Lean4

theorem comp_hasDerivWithinAt_of_eq (hl : HasFDerivAt l l' y) (hf : HasDerivWithinAt f f' s x) (hy : y = f x) :
    HasDerivWithinAt (l ∘ f) (l' f') s x := by rw [hy] at hl; exact hl.comp_hasDerivWithinAt x hf

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