mul — Mathlib

English

If a and b are differentiable on s, then their product a b is differentiable on s.

Русский

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

LaTeX

$$$\\text{DifferentiableOn}_{\\mathbb{K}}(a,s) \\land \\text{DifferentiableOn}_{\\mathbb{K}}(b,s) \\Rightarrow \\text{DifferentiableOn}_{\\mathbb{K}}(y \\mapsto a(y) b(y),s)$$$

Lean4

@[fun_prop]
theorem mul (ha : DifferentiableOn 𝕜 a s) (hb : DifferentiableOn 𝕜 b s) : DifferentiableOn 𝕜 (a * b) s := fun x hx =>
  (ha x hx).mul (hb x hx)

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