English
If α is a topological space with a continuous multiplication, then the product of a finite list, List.prod: List α → α, is continuous.
Русский
Если α — топологическое пространство с непрерывным умножением, то произведение списка List α по концу списка непрерывно по функции List.prod.
LaTeX
$$$\\\\forall {\\\\alpha}, [TopologicalSpace(\\\\alpha)], [MulOneClass(\\\\alpha)], [ContinuousMul(\\\\alpha)], \\\\text{Continuous}(\\\\text{List.prod} : \\\\text{List}(\\\\alpha) \\\\to \\\\alpha)$$$
Lean4
@[to_additive]
theorem tendsto_prod [MulOneClass α] [ContinuousMul α] {l : List α} : Tendsto List.prod (𝓝 l) (𝓝 l.prod) := by
induction l with
| nil => simp +contextual [nhds_nil, mem_of_mem_nhds, tendsto_pure_left]
| cons x l ih =>
simp_rw [tendsto_cons_iff, prod_cons]
have := continuous_iff_continuousAt.mp continuous_mul (x, l.prod)
rw [ContinuousAt, nhds_prod_eq] at this
exact this.comp (tendsto_id.prodMap ih)
