contMDiff_finprod — Mathlib

English

If hc ensures ContMDiff for each f_i under condition p_i, and hf is locally finite, then the conditional infinite product ∏ᶠ (i) (p i) f_i is ContMDiff.

Русский

Если выполнено условие hc для каждого f_i с условием p_i и hf локально кончен, то условное бесконечное произведение ContMDiff.

LaTeX

$$$(\text{hc } : \forall i, p i \to ContMDiff I' I n (f_i)) (hf : LocallyFinite (\lambda i, mulSupport (f_i))) \,\to \, ContMDiff I' I n (\prod^{\!\!f}_{i} f_i)$$$

Lean4

@[to_additive]
theorem contMDiff_finprod (h : ∀ i, ContMDiff I' I n (f i)) (hfin : LocallyFinite fun i => mulSupport (f i)) :
    ContMDiff I' I n fun x => ∏ᶠ i, f i x := fun x ↦ contMDiffAt_finprod hfin fun i ↦ h i x

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