English
Let φ: ι' → ι. The equality of uniform spaces states that the comap of the Pi-space along precomposition with φ equals the infimum of the comaps along the evaluations at φ i'.
Русский
Пусть φ: ι' → ι. Равенство пространств равномерности утверждает, что comap пространства Pi по предкомпозиции с φ равен infimum по всем i' от comap по eval (φ i').
LaTeX
$$$UniformSpace.comap (fun g i' \\mapsto g(\\varphi i')) (Pi.uniformSpace (fun i' \\mapsto \\alpha(\\varphi i'))) = ⨅ i', UniformSpace.comap (eval(\\varphi i')) (U(\\varphi i'))$$$
Lean4
theorem uniformSpace_comap_precomp' (φ : ι' → ι) :
UniformSpace.comap (fun g i' ↦ g (φ i')) (Pi.uniformSpace (fun i' ↦ α (φ i'))) =
⨅ i', UniformSpace.comap (eval (φ i')) (U (φ i')) :=
by simp [Pi.uniformSpace_eq, UniformSpace.comap_iInf, ← UniformSpace.comap_comap, comp_def]
