comap_coe_eq_uniformity — Mathlib

English

The uniformity on α is obtained by pulling back the uniformity from Completion α along the inclusion α → Completion α.

Русский

Равномерность на α получается как прообраз равномерности на Completion α по включению α → Completion α.

LaTeX

$$$\\mathcal U_{\\alpha} = \\mathrm{comap}_{(\\iota\\times\\iota)}\\, \\mathcal U_{\\mathrm{Completion}(\\alpha)}$$$

Lean4

theorem comap_coe_eq_uniformity : ((𝓤 _).comap fun p : α × α => ((p.1 : Completion α), (p.2 : Completion α))) = 𝓤 α :=
  (isUniformInducing_coe _).1

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