finset_prod — Mathlib

English

If HasDerivWithinAt holds for each factor, then the product has a HasDerivWithinAt with the same product-rule form.

Русский

Если для каждой f_i существует HasDerivWithinAt, то произведение имеет 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) $$

Lean4

@[fun_prop]
theorem finset_prod (hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) : DifferentiableAt 𝕜 (∏ i ∈ u, f i) x := by
  convert DifferentiableAt.fun_finset_prod hd; simp

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