English
Let α_i be spaces each with a UniformSpace structure, and φ: ι' → ι be a map between index sets. Then the map that sends a family f = (f_i)_{i∈ι} to the family j ↦ f_{φ(j)} (i.e., precomposition with φ) is uniformly continuous from the product space ∏_{i∈ι} α_i to ∏_{j∈ι'} α_{φ(j)}.
Русский
Пусть для каждого i ∈ ι задано пространство α_i с униформной структурой, и пусть φ: ι' → ι. Тогда отображение, отправляющее семейство f = (f_i)_{i∈ι в} в семейство j ↦ f_{φ(j)} (предкомпозиция с φ), является равномерно непрерывным из пространства произведения ∏_{i∈ι} α_i в ∏_{j∈ι'} α_{φ(j)}.
LaTeX
$$$UniformContinuous\\big( f \\mapsto (j \\mapsto f(\\varphi(j))) \\big)$$$
Lean4
theorem uniformContinuous_precomp' (φ : ι' → ι) : UniformContinuous (fun (f : (∀ i, α i)) (j : ι') ↦ f (φ j)) :=
uniformContinuous_pi.mpr fun j ↦ uniformContinuous_proj α (φ j)
