Commit 2024-08-19 07:41 047121fd

View on Github →

feat(Order/SuccPred/Basic): succ_eq_sInf (#15907) We prove that the successor of an element is the infimum of those greater than it, both in a complete lattice and a conditionally complete lattice with no maxima.

Estimated changes

added theorem Order.pred_eq_csSup
modified theorem Order.pred_eq_iSup
added theorem Order.pred_eq_sSup
added theorem Order.succ_eq_csInf
modified theorem Order.succ_eq_iInf
added theorem Order.succ_eq_sInf