Commit 2024-09-05 08:22 f91e7897

View on Github →

feat(Order/Max): basic IsMin / IsBot lemmas (#16453)

Estimated changes

Modified Mathlib/Order/Directed.lean

modified theorem exists_lt_of_directed_ge

modified theorem exists_lt_of_directed_le

Modified Mathlib/Order/Max.lean