English
If each f_i has a HasDerivWithinAt at x with derivative f_i'(x), then the product has a HasDerivWithinAt with derivative given by the standard product rule sum.
Русский
Если каждая f_i имеет производную внутри s в x с производной f_i'(x), тогда произведение имеет производную внутри s согласно стандартному правилу произведения.
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) $$
Lean4
theorem fun_finset_prod (hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x) :
HasDerivWithinAt (∏ i ∈ u, f i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x := by
simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
(HasFDerivWithinAt.finset_prod (fun i hi ↦ (hf i hi).hasFDerivWithinAt)).hasDerivWithinAt
