Theorem List.Sorted.lt_ord_of_lt

Modification history

2024-11-04 23:02
Mathlib/SetTheory/Ordinal/Basic.lean
chore(*): `LinearOrder` + `IsWellOrder α (· < ·)` → `LinearOrder` + `WellFoundedLT` (#18217) …
Modified List.Sorted.lt_ord_of_ltView on Github →
2023-10-26 10:03
Mathlib/SetTheory/Ordinal/Basic.lean
feat: condition for being < an ordinal in a decreasing list (#7899)
Added List.Sorted.lt_ord_of_ltView on Github →