smul — Mathlib

English

Let f: M → 𝕜 and g: M → V be differentiable at x. Then the product p ↦ f(p) · g(p) is differentiable at x.

Русский

Пусть f: M → 𝕜 и g: M → V дифференцируемы в точке x. Тогда p ↦ f(p) · g(p) дифференцируема в x.

LaTeX

$$$MDifferentiableAt I 𝓘(𝕜) f x \\;\\land\\; MDifferentiableAt I 𝓘(𝕜, V) g x \\Rightarrow MDifferentiableAt I 𝓘(𝕜, V) (\\\\lambda p. f p \\cdot g p) x$$$

Lean4

theorem smul {f : M → 𝕜} {g : M → V} (hf : MDifferentiableAt I 𝓘(𝕜) f x) (hg : MDifferentiableAt I 𝓘(𝕜, V) g x) :
    MDifferentiableAt I 𝓘(𝕜, V) (fun p => f p • g p) x :=
  ((contMDiff_smul.of_le le_top).mdifferentiable le_rfl _).comp x (hf.prodMk hg)

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