unop_bijective — Mathlib

English

Let α be a type. The map unop: α^{op} → α is bijective; hence α^{op} is canonically isomorphic to α.

Русский

Пусть α — множество. Отображение unop: α^{op} → α является биекцией; следовательно, α^{op} естественным образом изоморфно α.

LaTeX

$$$\\\\operatorname{Bijective}(\\\\mathrm{unop} : \\\\alpha^{\\\\mathrm{op}} \\\\to \\\\alpha)$$$

Lean4

@[to_additive]
theorem unop_bijective : Bijective (unop : αᵐᵒᵖ → α) :=
  opEquiv.symm.bijective

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