comap_uniformity_mulOpposite — Mathlib

English

The comap of MulOpposite.map with 𝓤 αᵐᵒᵖ along the op gives back 𝓤 α.

Русский

Комап MulOpposite.map с 𝓤 αᵐᵒᵖ по op возвращает 𝓤 α.

LaTeX

$$$$\\mathrm{comap}\\big( (\\lambda p: α \\times α, (MulOpposite.op p.1, MulOpposite.op p.2)) \\big) (\\mathcal{U}(α^{\\mathrm{op}})) = \\mathcal{U}(α).$$$$

Lean4

@[to_additive (attr := simp)]
theorem comap_uniformity_mulOpposite [UniformSpace α] :
    comap (fun p : α × α => (MulOpposite.op p.1, MulOpposite.op p.2)) (𝓤 αᵐᵒᵖ) = 𝓤 α := by
  simpa [uniformity_mulOpposite, comap_comap, (· ∘ ·)] using comap_id

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