Commit 2026-09-22 12:37 47644f4b
View on Github →feat(Order/ConditionallyCompleteLattice/Indexed): ≤ version of ciSup_or' for ConditionallyCompleteLattice (#38855)
Unprime ciSup_or' because there's no ciSup_or, and add a ≤ version (and dual) for ConditionallyCompleteLattice.
Only ≤ because equality does not hold when p ≠ q without sSup ∅ = ⊥.