Theorem bot_lt_of_lt

Modification history

2025-12-05 13:19
Mathlib/Order/BoundedOrder/Basic.lean
chore(Order/BoundedOrder/Basic): use `to_dual` (#32377) …
Deleted bot_lt_of_ltView on Github →
2024-09-14 06:53
Mathlib/Order/BoundedOrder.lean
feat (Order/BoundedOrder): add bot_lt_of_gt (#16660)
Added bot_lt_of_ltView on Github →