Commit 2026-03-15 22:43 02730e27

View on Github →

refactor: redefine Order.cof for a preorder (#35513) ... instead of using an unbundled relation. This makes it easier to work with, and avoids some swap rᶜ incantations. There are still a bunch of lemmas that make use of unbundled order relations; these will get fixed in follow-up PRs.

Estimated changes

modified theorem IsCofinal.singleton_top
modified def Order.cof
added theorem Order.cof_eq
added theorem Order.cof_eq_one
added theorem Order.cof_eq_one_iff
added theorem Order.cof_eq_zero
added theorem Order.cof_eq_zero_iff
modified theorem Order.cof_le
added theorem Order.cof_ne_zero
added theorem Order.cof_ne_zero_iff
deleted theorem Order.le_cof
added theorem Order.le_cof_iff
added theorem OrderIso.cof_eq
added theorem OrderIso.lift_cof_eq
modified theorem Ordinal.cof_eq'
deleted theorem Ordinal.cof_eq
deleted theorem Ordinal.cof_eq_cof_toType
added theorem Ordinal.cof_eq_one_iff
modified theorem Ordinal.cof_eq_zero
modified theorem Ordinal.cof_le_card
modified theorem Ordinal.cof_succ
added theorem Ordinal.cof_toType
modified theorem Ordinal.cof_type
deleted theorem Ordinal.cof_type_le
deleted theorem Ordinal.cof_type_lt
modified theorem Ordinal.cof_zero
deleted theorem Ordinal.le_cof_type
modified theorem Ordinal.lift_cof
deleted theorem Ordinal.lt_cof_type
modified theorem Ordinal.ord_cof_eq
modified theorem Ordinal.ord_cof_le
deleted theorem RelIso.cof_eq
deleted theorem RelIso.cof_eq_lift