English
If each f_i tends to a_i along a filter x for i in a finite index set s, then the product over i∈s tends to the product of a_i.
Русский
Если для каждого i в конечном наборе индексов s отображение f_i сходится к a_i вдоль фильтра x, то произведение по i∈s сходится к произведению a_i.
LaTeX
$$$\\forall i \\in s,\\ Tendsto (f i) x (\\mathcal{N}(a i)) \\Rightarrow \\ Tendsto (\\lambda b, \\prod_{i \\in s} f i b) x (\\mathcal{N}(\\prod_{i \in s} a i))$$$
Lean4
@[to_additive]
theorem tendsto_finset_prod {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι) :
(∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) → Tendsto (fun b => ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c)) :=
tendsto_multiset_prod _
