Theorem ltByCases_not_lt

Modification history

2025-10-31 08:47

Mathlib/Order/Basic.lean

chore: remove declarations deprecated before 2025-04-21 (#30759) …

Deleted ltByCases_not_lt View on Github →

2024-01-12 12:47

Mathlib/Order/Basic.lean

feat(Order/Basic): Add `ltByCases` API (#9114) …

Added ltByCases_not_lt View on Github →