mul_const' — Mathlib

English

If c and d are differentiable within s at x, then fderivWithin 𝕜 (fun y => c(y) * d(y)) s x equals c(x) • fderivWithin d s x plus d x • fderivWithin c s x.

Русский

Если функции c и d дифференцируемы внутри s в x, то fderivWithin 𝕜 (λ y, c(y) d(y)) s x равно c(x) • fderivWithin d s x плюс d(x) • fderivWithin c s x.

LaTeX

$$$\\forall hxs hc hd,\\ fderivWithin 𝕜 (y \\mapsto c(y) d(y)) s x = c(x) \\cdot fderivWithin 𝕜 d s x + d(x) \\cdot fderivWithin 𝕜 c s x$$$

Lean4

@[fun_prop]
theorem mul_const' (ha : HasFDerivAt a a' x) (b : 𝔸) : HasFDerivAt (fun y => a y * b) (a' <• b) x :=
  ((ContinuousLinearMap.mul 𝕜 𝔸).flip b).hasFDerivAt.comp x ha

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