English
Let f_i: X → M be a family of maps indexed by a finite list l ⊂ ι. If every f_i is continuous on a set t ⊆ X, then the map a ↦ ∏_{i ∈ l} f_i(a) is continuous on t.
Русский
Пусть f_i : X → M заданы для конечного набора индексов l ⊆ ι. Если для каждого i ∈ l отображение f_i непрерывно на t ⊆ X, то отображение a ↦ ∏_{i ∈ l} f_i(a) непрерывно на t.
LaTeX
$$$\\forall F \\subseteq \\iota\\,\\text{Finite}(F)\\;\\Big(\\forall i \\in F,\\ \\text{ContinuousOn}(f_i,t)\\Big) \\Rightarrow \\text{ContinuousOn}\\left( a \\mapsto \\prod_{i \\in F} f_i(a) , t\\right)$$$
Lean4
@[to_additive]
theorem continuousOn_list_prod {f : ι → X → M} (l : List ι) {t : Set X} (h : ∀ i ∈ l, ContinuousOn (f i) t) :
ContinuousOn (fun a => (l.map fun i => f i a).prod) t :=
by
intro x hx
rw [continuousWithinAt_iff_continuousAt_restrict _ hx]
refine tendsto_list_prod _ fun i hi => ?_
specialize h i hi x hx
rw [continuousWithinAt_iff_continuousAt_restrict _ hx] at h
exact h
