fun_mul' — Mathlib

English

If hc: DifferentiableAt 𝕜 c x, then fderiv 𝕜 (fun y => c(y) · f) x = (fderiv 𝕜 c x).smulRight f.

Русский

Если c дифференцируема в x, то производная функции y ↦ c(y) · f равна smulRight применённой к производной c, то есть (fderiv 𝕜 c x).smulRight f.

LaTeX

$$$\DifferentiableAt\ 𝕜\ c\ x \Rightarrow fderiv 𝕜 (\\lambda y. c(y) \\cdot f) x = (fderiv 𝕜 c x).smulRight f$$$

Lean4

@[fun_prop]
theorem fun_mul' (ha : HasFDerivAt a a' x) (hb : HasFDerivAt b b' x) :
    HasFDerivAt (fun y => a y * b y) (a x • b' + a' <• b x) x := by
  -- `by exact` to solve unification issues.
  exact ((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasFDerivAt (a x, b x)).comp x (ha.prodMk hb)

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