Commit 2024-09-14 06:53 1ea941a9

View on Github →

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

Estimated changes

Modified Mathlib/Order/BoundedOrder.lean

added theorem bot_lt_of_lt

added theorem lt_top_of_lt