Commit 2023-10-26 10:03 c6cb8b61

View on Github →

feat: condition for being < an ordinal in a decreasing list (#7899)

Estimated changes

Modified Mathlib/Data/List/Lex.lean

modified theorem List.head!_le_of_lt

added theorem List.head_le_of_lt

Modified Mathlib/SetTheory/Ordinal/Basic.lean

added theorem List.Sorted.lt_ord_of_lt