Commit 2026-05-10 00:45 7d6fdac1
View on Github →feat(Order/ConditionallyCompleteLattice/Indexed): conditional versions of iSup_exists/iSup_and (#38857)
For iSup_exists we can only get ≤ in ConditionallyCompleteLattice, and equality in ConditionallyCompleteLinearOrderBot.