smul — Mathlib

English

If HasDerivWithinAt c c' s x and HasDerivWithinAt f f' s x, then HasDerivWithinAt (c • f) (c x • f' + c' • f x) s x.

Русский

Если HasDerivWithinAt c c' s x и HasDerivWithinAt f f' s x, то HasDerivWithinAt (c • f) выражается как c(x) f'(x) плюс c'(x) f(x).

LaTeX

$$$\text{HasDerivWithinAt } c c' s x \to \text{HasDerivWithinAt } f f' s x \to \text{HasDerivWithinAt } (c \cdot f) (c x \cdot f' + c' \cdot f x) s x$$$

Lean4

theorem smul (hc : HasDerivWithinAt c c' s x) (hf : HasDerivWithinAt f f' s x) :
    HasDerivWithinAt (c • f) (c x • f' + c' • f x) s x := by simpa using (HasFDerivWithinAt.smul hc hf).hasDerivWithinAt

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