fun_mul — Mathlib

English

If a and b are differentiable, then their product 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) b(y))$$$

Lean4

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

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