mul_const — Mathlib

English

If hc and hd are HasDerivWithinAt for c and d, then the product has a derivative within s given by c' d(x) + c(x) d'.

Русский

Если hc и hd задают производную внутри множества для c и d, то произведение имеет внутри s производную, равную c'(x) d(x) + c(x) d'(x).

LaTeX

$$$\text{HasDerivWithinAt}(c \cdot d)\, s\, x = c'(x) d(x) + c(x) d'(x)$$$

Lean4

theorem mul_const (hc : HasDerivWithinAt c c' s x) (d : 𝔸) : HasDerivWithinAt (fun y => c y * d) (c' * d) s x :=
  by
  convert hc.mul (hasDerivWithinAt_const x s d) using 1
  rw [mul_zero, add_zero]

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