fun_mul — Mathlib

English

Let a, b: E → 𝔸 be differentiable on a set s. Then the product y ↦ a(y) b(y) is differentiable on s.

Русский

Пусть a, b: E → 𝔸 — функции, дифференцируемые на множествах s. Тогда произведение y ↦ a(y) b(y) дифференцируемо на 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 fun_mul (ha : DifferentiableOn 𝕜 a s) (hb : DifferentiableOn 𝕜 b s) :
    DifferentiableOn 𝕜 (fun y => a y * b y) s := fun x hx => (ha x hx).mul (hb x hx)

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