English
Same as above, expressed with derivWithin for a finite product of differentiable factors.
Русский
То же самое, что и выше, выраженное через derivWithin для конечного произведения дифференцируемых множителей.
LaTeX
$$$ \mathrm{derivWithin}( \prod_{i \in u} f_i(x) ) = \sum_{i \in u} \left( \prod_{j \in u \setminus \{i\}} f_j(x) \right) \mathrm{derivWithin}( f_i)(x) $$$
Lean4
theorem derivWithin_fun_finset_prod (hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) :
derivWithin (∏ i ∈ u, f i ·) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (HasDerivWithinAt.fun_finset_prod fun i hi ↦ (hf i hi).hasDerivWithinAt).derivWithin hsx
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
