Theorem lt_top_of_lt

Modification history

2025-12-05 13:19

Mathlib/Order/BoundedOrder/Basic.lean

chore(Order/BoundedOrder/Basic): use `to_dual` (#32377) …

Modified lt_top_of_lt View on Github →

2024-09-14 06:53

Mathlib/Order/BoundedOrder.lean

feat (Order/BoundedOrder): add bot_lt_of_gt (#16660)

Added lt_top_of_lt View on Github →