Theorem List.Sorted.lt_ord_of_lt

Modification history

2025-12-05 15:16
Mathlib/SetTheory/Ordinal/Basic.lean
refactor(`Data/List/Sort`): deprecate and replace `List.Sorted` (#30441) …
Deleted List.Sorted.lt_ord_of_ltView on Github →
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 →