Commit 2026-02-24 13:32 900da3d0

View on Github →

feat: more lemmas on Ordinal.type (#35519) Extracted from #35513.

Estimated changes

Modified Mathlib/Order/Max.lean

added theorem noBotOrder_iff

added theorem noMinOrder_iff

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

added theorem Ordinal.isSuccPrelimit_type_lt

added theorem Ordinal.isSuccPrelimit_type_lt_iff

added theorem Ordinal.type_lt_mem_range_succ

added theorem Ordinal.type_lt_mem_range_succ_iff

added theorem Ordinal.type_lt_ulift

deleted theorem Ordinal.type_uLift

added theorem Ordinal.type_ulift