Theorem BddBelow.exists_isLeast_of_nonempty

Modification history

2026-02-22 13:15

Mathlib/Order/SuccPred/Archimedean.lean

chore(Order/SuccPred/Archimedean): use `to_dual` (#34882)

Deleted BddBelow.exists_isLeast_of_nonempty View on Github →

2024-10-09 09:42

Mathlib/Order/SuccPred/Archimedean.lean

feat(Order/SuccPred): `BddAbove.exists_isGreatest_of_nonempty` (#15944) …

Added BddBelow.exists_isLeast_of_nonempty View on Github →