English
For a map φ: ι' → ι, the uniform structure on the space of functions obtained by precomposition, UniformSpace.comap (fun g i' => g(φ i')) (Pi.uniformSpace (fun i' => α(φ i'))), equals the infimum over i' of UniformSpace.comap (eval (φ i')) (U(φ i')).
Русский
Для отображения φ: ι' → ι равномерная структура на пространстве функций, полученная предкомпозицией, равна наименьшему элементу по всем i' из UniformSpace.comap (eval(φ i')) (U(φ i')).
LaTeX
$$$UniformSpace.comap (fun g i' \\mapsto g(\\varphi i')) (Pi.uniformSpace (fun i' \\mapsto \\alpha(\\varphi i'))) = \\bigwedge_{i'} UniformSpace.comap (eval(\\varphi i')) (U(\\varphi i'))$$$
Lean4
theorem uniformContinuous_postcomp {α : Type*} [UniformSpace α] {g : α → β} (hg : UniformContinuous g) :
UniformContinuous (g ∘ · : (ι → α) → (ι → β)) :=
Pi.uniformContinuous_postcomp' _ fun _ ↦ hg
