smul — Mathlib

English

If f is differentiable on a set and g is differentiable on the same set, then the product p ↦ f(p) · g(p) is differentiable on that set.

Русский

Если функции f и g дифференцируемы на множествае s, то произведение p ↦ f(p) · g(p) дифференцируемо на этом множестве.

LaTeX

$$$MDifferentiableOn I 𝓘(𝕜) f s \\quad \\text{and} \\quad MDifferentiableOn I 𝓘(𝕜, V) g s \\quad \\Rightarrow \\quad MDifferentiableOn I 𝓘(𝕜, V) (\\lambda p. f(p) \\cdot g(p)) s$$$

Lean4

theorem smul {f : M → 𝕜} {g : M → V} (hf : MDifferentiableOn I 𝓘(𝕜) f s) (hg : MDifferentiableOn I 𝓘(𝕜, V) g s) :
    MDifferentiableOn I 𝓘(𝕜, V) (fun p => f p • g p) s := fun x hx => (hf x hx).smul (hg x hx)

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