uniformity_multiplicative — Mathlib

English

The uniformity on Multiplicative α is the pushforward of 𝓤 α via Prod.map(ofAdd, ofAdd).

Русский

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

LaTeX

$$$$\\mathcal{U}(\\mathrm{Multiplicative}(\\alpha)) = (\\mathcal{U}(\\alpha)).map(\\mathrm{Prod.map}(\\mathrm{ofAdd}, \\mathrm{ofAdd})).$$$$

Lean4

theorem uniformity_multiplicative : 𝓤 (Multiplicative α) = (𝓤 α).map (Prod.map ofAdd ofAdd) :=
  rfl

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