Commit 2024-10-09 09:42 23081567

View on Github →

feat(Order/SuccPred): BddAbove.exists_isGreatest_of_nonempty (#15944) when IsSuccArchimedean

Estimated changes

Modified Mathlib/Order/SuccPred/Archimedean.lean

added theorem BddAbove.exists_isGreatest_of_nonempty

added theorem BddBelow.exists_isLeast_of_nonempty