contMDiffWithinAt_finset_prod — Mathlib

English

If every i in t is ContMDiffWithinAt on s, then the product over t is ContMDiffWithinAt on s.

Русский

Если все i в t дают ContMDiffWithinAt на s, то произведение по t является ContMDiffWithinAt на s.

LaTeX

$$$\\\\forall i \\\\in t, \\\\ ContMDiffWithinAt I' I n (f_i) s x \\\\Rightarrow ContMDiffWithinAt I' I n (\\\\prod i \\\\in t, f_i) s x$$$

Lean4

@[to_additive]
theorem contMDiffWithinAt_finset_prod (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
    ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) s x :=
  by
  simp only [← Finset.prod_apply]
  exact contMDiffWithinAt_finset_prod' h

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