English
If f is MDifferentiableWithinAt valued in 𝕜 and g is MDifferentiableWithinAt valued in V on s, then the product f•g is MDifferentiableWithinAt on s at x.
Русский
Если f: M→𝕜 и g: M→V слабо дифференцируемы внутри s, то их произведение векторно-скалярное тоже дифференцируемо внутри s.
LaTeX
$$$\text{MDifferentiableWithinAt } I\ 𝓘(𝕜)\ f\ s\ x \land \text{MDifferentiableWithinAt } I\ 𝓘(𝕜, V)\ g\ s\ x \implies\ MDifferentiableWithinAt I\ 𝓘(𝕜, V)\ (\lambda p, f\, p \cdot g\, p)\ s\ x$$$
Lean4
theorem clm_prodMap {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} (hg : MDifferentiable I 𝓘(𝕜, F₁ →L[𝕜] F₃) g)
(hf : MDifferentiable I 𝓘(𝕜, F₂ →L[𝕜] F₄) f) :
MDifferentiable I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) fun x => (g x).prodMap (f x) := fun x => (hg x).clm_prodMap (hf x)
