fun_smul — Mathlib

English

Let c and f have strict derivatives at x, namely c'(x) and f'(x). Then the product y ↦ c(y) f(y) has strict derivative at x equal to c(x) f'(x) + c'(x) f(x).

Русский

Пусть c и f имеют строгие производные в точке x, соответственно c'(x) и f'(x). Тогда произведение y ↦ c(y) f(y) имеет строгую производную в x, равную c(x) f'(x) + c'(x) f(x).

LaTeX

$$$\\dfrac{d}{dy}\\bigl(c(y)f(y)\\bigr)\\text{ при } x = c(x)f'(x) + c'(x)f(x)$$$

Lean4

nonrec theorem fun_smul (hc : HasStrictDerivAt c c' x) (hf : HasStrictDerivAt f f' x) :
    HasStrictDerivAt (fun y => c y • f y) (c x • f' + c' • f x) x := by simpa using (hc.smul hf).hasStrictDerivAt

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