uniformity_additive — Mathlib

English

The additive uniformity is the pushforward of the original uniformity via Prod.map(ofMul, ofMul).

Русский

Равномерность Additive α получается как отображение через Prod.map(ofMul, ofMul) из 𝓤 α.

LaTeX

$$$$\\mathcal{U}(\\mathrm{Additive}(\\alpha)) = (\\mathcal{U}(\\alpha)).\\mathrm{map}(\\mathrm{Prod.map}(\\mathrm{ofMul}, \\mathrm{ofMul})).$$$$

Lean4

theorem uniformity_additive : 𝓤 (Additive α) = (𝓤 α).map (Prod.map ofMul ofMul) :=
  rfl

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