mul_const — Mathlib

English

If hxs, hc, hd hold, then fderivWithin 𝕜 (c * d) s x equals c(x) • fderivWithin d s x plus d(x) • fderivWithin c s x.

Русский

Пусть выполняются hxs, hc и hd; тогда fderivWithin 𝕜 (c d) s x равно c(x) • fderivWithin d s x плюс d(x) • fderivWithin c s x.

LaTeX

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

Lean4

@[fun_prop]
theorem mul_const (hc : HasFDerivWithinAt c c' s x) (d : 𝔸') : HasFDerivWithinAt (fun y => c y * d) (d • c') s x :=
  by
  convert hc.mul_const' d
  ext z
  apply mul_comm

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