English
The uniformity on the product α × β is the comap of the map sending ((a1,b1),(a2,b2)) to ((a1,a2),(b1,b2)) from (α × β) × α × β to α × α × β × β.
Русский
Униформность на произведении α × β равна прообразу (comap) отображения, отправляющего ((a1,b1),(a2,b2)) в ((a1,a2),(b1,b2)) из (α × β) × α × β в α × α × β × β.
LaTeX
$$$\mathcal{U}(\alpha \times \beta) = \mathrm{comap}\Big(\lambda p:(\alpha \times \beta) \times \alpha \times \beta.\, ((p.1.1,p.2.1),(p.1.2,p.2.2))\Big) (\mathcal{U}\alpha \times\mathcal{U}\beta)$$$
Lean4
theorem uniformity_prod_eq_comap_prod [UniformSpace α] [UniformSpace β] :
𝓤 (α × β) = comap (fun p : (α × β) × α × β => ((p.1.1, p.2.1), (p.1.2, p.2.2))) (𝓤 α ×ˢ 𝓤 β) := by
simp_rw [uniformity_prod, prod_eq_inf, Filter.comap_inf, Filter.comap_comap, Function.comp_def]
