mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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