English
If hc ensures ContMDiff for each i with predicate p i and hf is locally finite, then the conditioned finite product is ContMDiff.
Русский
Если для каждого i с предикатом p_i выполнено ContMDiff и hf локально кончен, то ограниченное конечное произведение дифференцируемо.
LaTeX
$$$(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_cond (hc : ∀ i, p i → ContMDiff I' I n (f i)) (hf : LocallyFinite fun i => mulSupport (f i)) :
ContMDiff I' I n fun x => ∏ᶠ (i) (_ : p i), f i x :=
by
simp only [← finprod_subtype_eq_finprod_cond]
exact contMDiff_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)
