derivWithin_finset_prod — Mathlib

English

If differentiableWithinAt for all factors, then the derivWithin of the finite product equals the product-rule sum.

Русский

Если для всех множителей имеется DifferentiableWithinAt, то производная внутри множества конечного произведения равна сумме по правилу произведения.

LaTeX

$$$ \mathrm{derivWithin}_s \left( \prod_{i \,\in \,u} f_i(x) \right) = \sum_{i \,\in \,u} \left( \prod_{j \,\in \,u \setminus \{i\}} f_j(x) \right) \mathrm{derivWithin}( f_i)(x) $$$

Lean4

theorem derivWithin_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
  convert derivWithin_fun_finset_prod hf; simp

Похожие утверждения