Commit 2024-11-12 03:03 8280f912

View on Github →

refactor(SetTheory/Cardinal/Cofinality): deprecate StrictOrder.cof (#18043) This definition is incorrect for partial orders and redundant for linear orders, see Zulip.

Estimated changes

deleted theorem Order.cof_nonempty
modified def Ordinal.cof
modified theorem Ordinal.cof_type
added theorem Ordinal.cof_type_lt