uniformity_prod — Mathlib

English

The uniformity on a product α × β is the infimum (greatest lower bound) of the comaps of the uniformities from α and β along the projections, i.e. 𝓤(α×β) equals the intersection of the two projected uniformities.

Русский

Равномерность на произведении α × β равна пересечению двух проекционных равномерностей.

LaTeX

$$$ 𝓤(\mathrm{Prod}\;\alpha\;\beta) = (𝓤\;\alpha)\mathrm{.comap}\;\mathrm{(fst, fst)} \; \cap \; (𝓤\;\beta)\mathrm{.comap}\; \mathrm{(snd, snd)} $$$

Lean4

theorem uniformity_prod [UniformSpace α] [UniformSpace β] :
    𝓤 (α × β) =
      ((𝓤 α).comap fun p : (α × β) × α × β => (p.1.1, p.2.1)) ⊓ (𝓤 β).comap fun p : (α × β) × α × β => (p.1.2, p.2.2) :=
  rfl

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