fun_mul — Mathlib

English

If ha: DifferentiableAt 𝕜 a x and hb: DifferentiableAt 𝕜 b x, then DifferentiableAt 𝕜 (y ↦ a(y) · b(y)) x.

Русский

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

LaTeX

$$$\text{DifferentiableAt } 𝕜\ a\ x \rightarrow \text{DifferentiableAt } 𝕜\ b\ x \rightarrow \text{DifferentiableAt } 𝕜\ (a(y) \cdot b(y))\ x$$$

Lean4

@[simp, fun_prop]
theorem fun_mul (ha : DifferentiableAt 𝕜 a x) (hb : DifferentiableAt 𝕜 b x) :
    DifferentiableAt 𝕜 (fun y => a y * b y) x :=
  (ha.hasFDerivAt.mul' hb.hasFDerivAt).differentiableAt

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