fun_finset_prod — Mathlib

English

If each f_i is differentiable at x, then the product ∏ f_i is differentiable at x.

Русский

Если каждая f_i дифференцируема в x, то произведение ∏ f_i дифференцируемо в x.

LaTeX

$$$ \text{Differentiable} \left( \prod_{i \in u} f_i, x \right)$$

Lean4

@[fun_prop]
theorem fun_finset_prod (hd : ∀ i ∈ u, Differentiable 𝕜 (f i)) : Differentiable 𝕜 (∏ i ∈ u, f i ·) := fun x ↦
  .fun_finset_prod (fun i hi ↦ hd i hi x)

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