English
Let (A_i) and (X_i) be families of topological spaces indexed by I, and for every i an individual map g_i : A_i → X_i which is continuous. Then the coordinatewise map F from the product ∏_{i∈I} A_i to ∏_{i∈I} X_i given by F((a_i)) = (g_i(a_i)) is continuous.
Русский
Пусть для множества индексов I данные семейства топологических пространств A_i и X_i, и для каждого i имеем непрерывную отображение g_i: A_i → X_i. Тогда координатно-образующая карта F: ∏_{i∈I} A_i → ∏_{i∈I} X_i, F((a_i)) = (g_i(a_i))_i, непрерывна.
LaTeX
$$$\\forall i,\\; g_i: A_i \\to X_i\\quad\\text{with } g_i \\text{ continuous} \\;\\\Rightarrow\\; \\text{Continuous}\\big( F:\\prod_{i} A_i \\to \\prod_{i} X_i,\\; F((a_i)_i) = (g_i(a_i))_i \\big).$$$
Lean4
theorem continuous_postcomp' {X : ι → Type*} [∀ i, TopologicalSpace (X i)] {g : ∀ i, A i → X i}
(hg : ∀ i, Continuous (g i)) : Continuous (fun (f : (∀ i, A i)) (i : ι) ↦ g i (f i)) :=
continuous_pi fun i ↦ (hg i).comp <| continuous_apply i
