Theorem cbiSup_eq_of_forall_not

Modification history

2026-04-05 08:48
Mathlib/Order/ConditionallyCompletePartialOrder/Indexed.lean
feat(Order/ConditionallyCompleteLattice): Generalize and add cbiSup/cbiInf theorems (#37526) …
Added cbiSup_eq_of_forall_notView on Github →