English
Let f : M → 𝕜 and g : M → V be differentiable-within-at at x on s in a C^n sense. Then the product map p ↦ f(p) · g(p) is differentiable-within-at at x on s.
Русский
Пусть f : M → 𝕜 и g : M → V дифференцируемы внутри x на s в смысле C^n. Тогда отображение p ↦ f(p) · g(p) дифференцируемо внутри x на s.
LaTeX
$$$\text{Let } f: M \to 𝕜 \text{ and } g: M \to V.\;\text{If } f \text{ and } g \text{ are differentiable within at } x \text{ on } s,\; \text{then } x \mapsto f(x) \cdot g(x) \\text{is differentiable within at } x \text{ on } s.$$$
Lean4
theorem smul {f : M → 𝕜} {g : M → V} (hf : MDifferentiableWithinAt I 𝓘(𝕜) f s x)
(hg : MDifferentiableWithinAt I 𝓘(𝕜, V) g s x) : MDifferentiableWithinAt I 𝓘(𝕜, V) (fun p => f p • g p) s x :=
((contMDiff_smul.of_le le_top).mdifferentiable le_rfl _).comp_mdifferentiableWithinAt x (hf.prodMk hg)
