opAddEquiv_toEquiv — Mathlib

English

The underlying equivalence of the additive opposite construction equals the standard opposite equivalence.

Русский

Пусть на типе A задано дополнение; соответствие opAddEquiv, как обычная эквивалентность между A и Aᵒᵖ, совпадает с обычной эквивалентностью opEquiv.

LaTeX

$$$\bigl(\text{opAddEquiv} : \alpha \simeq_+ \alpha^{\mathrm{op}}\bigr) \vert_\alpha = \text{opEquiv}$$$

Lean4

@[simp]
theorem opAddEquiv_toEquiv [Add α] : ((opAddEquiv : α ≃+ αᵐᵒᵖ) : α ≃ αᵐᵒᵖ) = opEquiv :=
  rfl

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