preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe'

English

The inverse component of a certain canonical isomorphism acts by the dual antisymmetrization on an element.

Русский

Обратная дуга канонического изоморфизма действует на элемент через двойственную антисимметризацию.

LaTeX

$$$(preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X)\; a = (OrderIso.dualAntisymmetrization \uparrow X).symm\; a$$$

Lean4

@[simp]
theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe' (X)
    (a : preordToPartOrd.obj (Preord.dual.obj X)) :
    (PartOrd.Hom.hom (X := preordToPartOrd.obj (Preord.dual.obj X)) (Y := PartOrd.dual.obj (preordToPartOrd.obj X))
          (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X))
        a =
      (OrderIso.dualAntisymmetrization ↑X).symm a :=
  rfl

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