English
If for each i ∈ ι there is a uniformly continuous map g_i: α_i → β_i, then the map sending f ∈ ∀ i, α_i to (i ↦ g_i(f(i))) ∈ ∀ i, β_i is uniformly continuous. More precisely, if hg: ∀ i, UniformContinuous (g_i), then the map f ↦ (i ↦ g_i(f(i))) is UniformContinuous.
Русский
Пусть для каждого i ∈ ι имеется равномерно непрерывная карта g_i: α_i → β_i. Тогда отображение f ∈ ∀ i, α_i к (i ↦ g_i(f(i))) ∈ ∀ i, β_i равномерно непрерывно.
LaTeX
$$(∀ i, UniformContinuous (g i)) ⇒ UniformContinuous (f ↦ (i ↦ g i (f i)))$$
Lean4
theorem uniformContinuous_postcomp' {β : ι → Type*} [∀ i, UniformSpace (β i)] {g : ∀ i, α i → β i}
(hg : ∀ i, UniformContinuous (g i)) : UniformContinuous (fun (f : (∀ i, α i)) (i : ι) ↦ g i (f i)) :=
uniformContinuous_pi.mpr fun i ↦ (hg i).comp <| uniformContinuous_proj α i
