Theorems · Theorem · order theory

preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe

∀ (X : Preord) (a : ↑((Preord.dual.comp preordToPartOrd).obj X)),
  (PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X)) a =
    (OrderIso.dualAntisymmetrization ↑X).symm a

Defined in

Mathlib.Order.Category.PartOrd

Cited by

0 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound