fun_mul — Mathlib

English

If ha: DifferentiableWithinAt 𝕜 a s x and hb: DifferentiableWithinAt 𝕜 b s x, then y ↦ a(y) · b(y) is DifferentiableWithinAt 𝕜 at x on s.

Русский

Если a и b дифференцируемы внутри s в x, то произведение y ↦ a(y) · b(y) дифференцируема внутри s в x.

LaTeX

$$$\text{DifferentiableWithinAt } 𝕜\ a\ s\ x \rightarrow \text{DifferentiableWithinAt } 𝕜\ b\ s\ x \rightarrow \text{DifferentiableWithinAt } 𝕜\ (instHMul.hMul (a y) (b y))\ s\ x$$$

Lean4

@[fun_prop]
theorem fun_mul (ha : DifferentiableWithinAt 𝕜 a s x) (hb : DifferentiableWithinAt 𝕜 b s x) :
    DifferentiableWithinAt 𝕜 (fun y => a y * b y) s x :=
  (ha.hasFDerivWithinAt.mul' hb.hasFDerivWithinAt).differentiableWithinAt

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