English
If each f_i: X → M is continuous, then the map a ↦ ∏_i f_i(a) (finite product) is continuous.
Русский
Если каждое f_i: X → M непрерывно, то отображение a ↦ ∏_i f_i(a) является непрерывным (пределенный конечный набор факторов).
LaTeX
$$$\text{ContinuousListProd}:\;\forall l,\ (\forall i \in l, Continuous (f i)) \Rightarrow Continuous (\lambda a, (l.map (\lambda i, f i a)).prod)$$$
Lean4
@[to_additive (attr := continuity, fun_prop)]
theorem continuous_list_prod {f : ι → X → M} (l : List ι) (h : ∀ i ∈ l, Continuous (f i)) :
Continuous fun a => (l.map fun i => f i a).prod :=
continuous_iff_continuousAt.2 fun x => tendsto_list_prod l fun c hc => continuous_iff_continuousAt.1 (h c hc) x
