contMDiffWithinAt_finset_prod' — Mathlib

English

If every i in t satisfies ContMDiffWithinAt, then the finite product over t is ContMDiffWithinAt.

Русский

Если каждый i в t удовлетворяет ContMDiffWithinAt, то конечное произведение над t является ContMDiffWithinAt.

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 (∏ i ∈ t, f i) s x :=
  Finset.prod_induction f (fun f => ContMDiffWithinAt I' I n f s x) (fun _ _ hf hg => hf.mul hg)
    (contMDiffWithinAt_const (c := 1)) h

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