English
If f_i : X → M and p_i are predicates such that p_i is true for all i in some finite set and each f_i is continuous on that subset, then the finite product over i with p_i is continuous as a function of x.
Русский
Если f_i : X → M и p_i — предикаты, и существует конечный поднабор индексов, где p_i истинно и каждый f_i непрерывна на этом подмножестве, то финальное произведение по этим i непрерывно зависит от x.
LaTeX
$$$\\text{Continuous}\ \bigl( x \\mapsto \\prod^\\! i\\ f_i(x) \\bigr)$ над условием $p_i$ и локальной конечностью$$
Lean4
@[to_additive]
theorem continuous_finprod_cond {f : ι → X → M} {p : ι → Prop} (hc : ∀ i, p i → Continuous (f i))
(hf : LocallyFinite fun i => mulSupport (f i)) : Continuous fun x => ∏ᶠ (i) (_ : p i), f i x :=
by
simp only [← finprod_subtype_eq_finprod_cond]
exact continuous_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)
