uniformity_comap — Mathlib

English

For any f: α → β, the uniformity on the comap space equals the comap of the uniformity by Prod.map f f: 𝓤[UniformSpace.comap f] = comap (Prod.map f f) (𝓤 β).

Русский

Для любого отображения f: α → β униформность пространства comap равна обратному отображению униформности через Prod.map f f: 𝓤[UniformSpace.comap f] = comap (Prod.map f f) (𝓤 β).

LaTeX

$$$\mathcal{U}[UniformSpace.comap f] = \operatorname{comap} (\\Prod.map f f) (\\mathcal{U} β)$$$

Lean4

theorem uniformity_comap {_ : UniformSpace β} (f : α → β) : 𝓤[UniformSpace.comap f ‹_›] = comap (Prod.map f f) (𝓤 β) :=
  rfl

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