Theorem BddAbove.exists_isGreatest_of_nonempty

Modification history

2024-10-09 09:42
Mathlib/Order/SuccPred/Archimedean.lean
feat(Order/SuccPred): `BddAbove.exists_isGreatest_of_nonempty` (#15944) …
Added BddAbove.exists_isGreatest_of_nonemptyView on Github →