English
Let s be a finite set of indices ι. If f i → a i for each i ∈ s and each a i ≠ ∞, then the finite product ∏ c ∈ s f c converges to ∏ c ∈ s a c.
Русский
Пусть s — конечное множество индексов, если f i → a i для каждого i ∈ s и каждый a i ≠ ∞, то произведение ∏ c ∈ s f c сходится к ∏ c ∈ s a c.
LaTeX
$$$\\\\forall s: Finset ι, (\\\\forall i ∈ s, Tendsto (f i) x (nhds (a i))) \\\\land (\\\\forall i ∈ s, a i ≠ ∞) \\\\Rightarrow \\\\ Tendsto (\\\\lambda b, \\\\prod c ∈ s, f c b) x (nhds (\\\\prod c ∈ s, a c)).$$$
Lean4
theorem tendsto_finset_prod_of_ne_top {ι : Type*} {f : ι → α → ℝ≥0∞} {x : Filter α} {a : ι → ℝ≥0∞} (s : Finset ι)
(h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞) :
Tendsto (fun b => ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c)) := by
classical
induction s using Finset.induction with
| empty => simp [tendsto_const_nhds]
| insert _ _ has IH =>
simp only [Finset.prod_insert has]
apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
· right
exact prod_ne_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)
· exact IH (fun i hi => h _ (Finset.mem_insert_of_mem hi)) fun i hi => h' _ (Finset.mem_insert_of_mem hi)
· exact Or.inr (h' _ (Finset.mem_insert_self _ _))
