English
Let a,b be differentiable within s at x. Then the derivative within s of a b at x satisfies D(a b) = a(x) · Db + Da · b(x).
Русский
Пусть a, b дифференцируемы внутри s в точке x. Тогда внутри s производная от произведения a b удовлетворяет равенству D(a b) = a(x) Db + Da b(x).
LaTeX
$$$\\forall x\\,\\text{UniqueDiffWithinAt}_{\\mathbb{K}}(s,x)\\,\\forall a,b\\,\\big( \\text{DifferentiableWithinAt}_{\\mathbb{K}} a s x \\to \\text{DifferentiableWithinAt}_{\\mathbb{K}} b s x \\to\\ fderivWithin_{\\mathbb{K}}(y\\mapsto a(y) b(y))\,s\,x = a(x) \\cdot fderivWithin_{\\mathbb{K}} b s x + fderivWithin_{\\mathbb{K}} a s x \\cdot<\\!\\!\\!> b(x) \\big)$$$
Lean4
theorem fderivWithin_fun_mul' (hxs : UniqueDiffWithinAt 𝕜 s x) (ha : DifferentiableWithinAt 𝕜 a s x)
(hb : DifferentiableWithinAt 𝕜 b s x) :
fderivWithin 𝕜 (fun y => a y * b y) s x = a x • fderivWithin 𝕜 b s x + fderivWithin 𝕜 a s x <• b x :=
(ha.hasFDerivWithinAt.mul' hb.hasFDerivWithinAt).fderivWithin hxs
