finset_prod — Mathlib

English

If each f_i is differentiable at x, then the finite 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 finset_prod (hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) : DifferentiableWithinAt 𝕜 (∏ i ∈ u, f i) s x :=
  by convert DifferentiableWithinAt.fun_finset_prod hd; simp

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