mul — Mathlib

English

If a and b are differentiable, then a * b is differentiable.

Русский

Если функции a и b дифференцируемы, то их произведение a b дифференцируемо.

LaTeX

$$$\\text{Differentiable}_{\\mathbb{K}}(a) \\land \\text{Differentiable}_{\\mathbb{K}}(b) \\Rightarrow \\text{Differentiable}_{\\mathbb{K}}(y \\mapsto a(y) \\cdot b(y))$$$

Lean4

@[simp, fun_prop]
theorem mul (ha : Differentiable 𝕜 a) (hb : Differentiable 𝕜 b) : Differentiable 𝕜 (a * b) := fun x => (ha x).mul (hb x)

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