English
If each f_i tends to a_i along a filter x, then the product over i in a finite multiset s tends to the product of the a_i along x.
Русский
Если для каждого i ∈ s отображение f_i сходится к a_i вдоль фильтра x, то произведение по i в мультисете s сходится к произведению a_i вдоль x.
LaTeX
$$$\\forall i \\in s,\\ Tendsto (f i) x (\\mathcal{N}(a i))\\Rightarrow \\ Tendsto (\\lambda b, (s.map (\\lambda c, f c b) ).prod) x (\\mathcal{N}(s.map a).prod)$$$
Lean4
@[to_additive]
theorem tendsto_multiset_prod {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι) :
(∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) → Tendsto (fun b => (s.map fun c => f c b).prod) x (𝓝 (s.map a).prod) :=
by
rcases s with ⟨l⟩
simpa using tendsto_list_prod l
