contMDiffAt_finprod — Mathlib

English

Similarly to the previous, a finprod over i of ContMDiffAt functions is ContMDiffAt at x0.

Русский

Аналогично предыдущему: финальное произведение функций ContMDiffAt по i в точке x0 также ContMDiffAt.

LaTeX

$$$\\\\contMDiffAt I I n (finprod i, f_i) x_0$ iff appropriate hypotheses$$

Lean4

@[to_additive]
theorem contMDiffAt_finprod (lf : LocallyFinite fun i ↦ mulSupport <| f i) (h : ∀ i, ContMDiffAt I' I n (f i) x₀) :
    ContMDiffAt I' I n (fun x ↦ ∏ᶠ i, f i x) x₀ :=
  contMDiffWithinAt_finprod lf h

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