English
Let f_i: α → M for i in ι and a_i ∈ M. If the nets Tendsto f_i to a_i along x for all i in a finite list l, then the product over l tends to the product of the a_i along x.
Русский
Пусть для каждого i в списке l функциf_i: α→M и точки a_i ∈ M. Если Tendsto f_i к a_i вдоль фильтра x для каждого i, входящего в l, то произведение по элементам списка сходится к произведению a_i вдоль x.
LaTeX
$$$\forall l:\, List\, ι,\ (\forall i\in l, Tendsto (f i) x (nhds (a i))) \Rightarrow Tendsto (\lambda b, (l.map (\lambda c, f c b)).prod) x (nhds (l.map a).prod)$$$
Lean4
@[to_additive]
theorem tendsto_list_prod {f : ι → α → M} {x : Filter α} {a : ι → M} :
∀ l : List ι,
(∀ i ∈ l, Tendsto (f i) x (𝓝 (a i))) → Tendsto (fun b => (l.map fun c => f c b).prod) x (𝓝 (l.map a).prod)
| [], _ => by simp [tendsto_const_nhds]
| f :: l, h => by
simp only [List.map_cons, List.prod_cons]
exact (h f List.mem_cons_self).mul (tendsto_list_prod l fun c hc => h c (List.mem_cons_of_mem _ hc))
