Theorem IsMax.not_lt

Modification history

2025-12-03 01:23

Mathlib/Order/Max.lean

feat(Order/Max): use `@[to_dual]` (#32059) …

Deleted IsMax.not_lt View on Github →

2025-06-07 15:55

Mathlib/Order/Max.lean

chore(Order): use new ge/gt naming convention - Part 2 (#25560) …

Modified IsMax.not_lt View on Github →

2022-11-18 04:15

Mathlib/Order/Max.lean

feat: port Order.Max (#567) …

Added IsMax.not_lt View on Github →