uniformity_prod_eq_prod — Mathlib

English

The uniformity on α × β is the map of the product of α- and β-uniformities along the pairing coordinate transformation.

Русский

Униформность на произведении α × β равна отображению произведения униформностей по парному отображению координат.

LaTeX

$$$\mathcal{U}(\alpha \times \beta) = \mathrm{map}\Big(\lambda p:(\alpha \times \alpha) \times \beta \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_prod [UniformSpace α] [UniformSpace β] :
    𝓤 (α × β) = map (fun p : (α × α) × β × β => ((p.1.1, p.2.1), (p.1.2, p.2.2))) (𝓤 α ×ˢ 𝓤 β) := by
  rw [map_swap4_eq_comap, uniformity_prod_eq_comap_prod]

Похожие утверждения