coe_dualDual_symm

Mathlib.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#OrderIso.coe_dualDual_symm

English

The dual of the dual, symmetrically, coincides with applying ofDual twice on the symmetric side.

Русский

Двойной двойной симметрии соответствует применению ofDual дважды на симметрической стороне.

LaTeX

$$$\mathrm{coe}_{\text{dualDual}}^{\text{symm}} = toDual^{-1} \circ toDual^{-1}$$$

Lean4

@[simp]
theorem coe_dualDual_symm : ⇑(dualDual α).symm = ofDual ∘ ofDual :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru