prod — Mathlib

English

If a locally finite family (f_i) has ContMDiffAt at x0, then the finprod is ContMDiffAt at x0.

Русский

Если локально конечно поддерживаемая совокупность функций имеет ContMDiffAt в точке x0, то их бесконечное произведение является ContMDiffAt в x0.

LaTeX

$$$\\\\forall i, ContMDiffAt I' I n (f_i) x_0 \\\\Rightarrow ContMDiffAt I' I n (\\\\lambda x, \\\\prod i, f_i(x)) x_0$$$

Lean4

@[to_additive]
theorem prod (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x₀) : ContMDiffAt I' I n (fun x ↦ ∏ i ∈ t, f i x) x₀ :=
  by
  simp only [← contMDiffWithinAt_univ] at *
  exact ContMDiffWithinAt.prod h

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