Commit 2023-07-31 11:35 fa6fd794

View on Github →

feat: Add basic order instances on ULift (#5998) This adds:

  • Preorder
  • PartialOrder
  • SemilatticeSup
  • SemilatticeInf
  • Lattice
  • DistribLattice
  • CompleteLattice
  • LinearOrder

Estimated changes

added theorem ULift.down_bot
added theorem ULift.down_top
added theorem ULift.up_bot
added theorem ULift.up_top
added theorem ULift.down_iInf
added theorem ULift.down_iSup
added theorem ULift.down_sInf
added theorem ULift.down_sSup
added theorem ULift.up_iInf
added theorem ULift.up_iSup
added theorem ULift.up_sInf
added theorem ULift.up_sSup
added theorem ULift.down_compare
added theorem ULift.down_compl
added theorem ULift.down_inf
added theorem ULift.down_le
added theorem ULift.down_lt
added theorem ULift.down_sdiff
added theorem ULift.down_sup
added theorem ULift.up_compare
added theorem ULift.up_compl
added theorem ULift.up_inf
added theorem ULift.up_le
added theorem ULift.up_lt
added theorem ULift.up_sdiff
added theorem ULift.up_sup