opEquiv — Mathlib

English

There is a canonical bijection between a type and its opposite type, given by the map op and its inverse unop.

Русский

Существует каноническое биективное соответствие между типом и его противоположным типом, задаваемое отображением op и его обратным unop.

LaTeX

$$$ \operatorname{opEquiv} : \alpha \simeq \alpha^{\mathrm{op}} $$$

Lean4

/-- The canonical bijection between `α` and `αᵐᵒᵖ`. -/
@[to_additive (attr := simps -fullyApplied apply symm_apply) /-- The canonical bijection between `α` and `αᵃᵒᵖ`. -/
    ]
def opEquiv : α ≃ αᵐᵒᵖ :=
  ⟨op, unop, unop_op, op_unop⟩

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