English
If each f_i has HasDerivWithinAt at x with derivative f_i'(x), then the product has HasDerivWithinAt with derivative given by the standard product-rule sum.
Русский
Если каждая f_i имеет HasDerivWithinAt в x с производной f_i'(x), то произведение имеет HasDerivWithinAt со производной, заданной суммой по правилу произведения.
LaTeX
$$$ \text{HasDerivWithinAt}\left( \prod_{i \in u} f_i, \; \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} f_j(x) \right) f_i'(x) \right) s x$$
Lean4
@[fun_prop]
theorem fun_finset_prod (hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) :
DifferentiableWithinAt 𝕜 (∏ i ∈ u, f i ·) s x := by
classical
exact
(HasDerivWithinAt.fun_finset_prod
(fun i hi ↦ DifferentiableWithinAt.hasDerivWithinAt (hd i hi))).differentiableWithinAt
