English
If hf1 and hf2 are differentiable within s at x, and s has unique differentiable point, then fderivWithin of the product equals product of fderivWithin: fderivWithin 𝕜 (λ x, (f1 x, f2 x)) s x = (fderivWithin 𝕜 f1 s x).prod (fderivWithin 𝕜 f2 s x).
Русский
Если hf1 и hf2 дифференцируемы внутри s в x и существует уникальная точка дифференцирования, то fderivWithin от произведения равна произведению fderivWithin.
LaTeX
$$$\text{fderivWithin } 𝕜 (\lambda x:E, (f_1 x,f_2 x)) s x = (\text{fderivWithin } 𝕜 f_1 s x).prod (\text{fderivWithin } 𝕜 f_2 s x)$$$
Lean4
theorem fderivWithin_prodMk (hf₁ : DifferentiableWithinAt 𝕜 f₁ s x) (hf₂ : DifferentiableWithinAt 𝕜 f₂ s x)
(hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun x : E => (f₁ x, f₂ x)) s x = (fderivWithin 𝕜 f₁ s x).prod (fderivWithin 𝕜 f₂ s x) :=
(hf₁.hasFDerivWithinAt.prodMk hf₂.hasFDerivWithinAt).fderivWithin hxs
