uniformity_mulOpposite — Mathlib

English

The uniformity on αᵐᵒᵖ is the comap of the original uniformity along MulOpposite.op mapping.

Русский

Равномерность на αᵐᵒᵖ есть композиция обратной по MulOpposite.op от 𝓤 α.

LaTeX

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

Lean4

@[to_additive]
theorem uniformity_mulOpposite [UniformSpace α] : 𝓤 αᵐᵒᵖ = comap (fun q : αᵐᵒᵖ × αᵐᵒᵖ => (q.1.unop, q.2.unop)) (𝓤 α) :=
  rfl

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