Theorem exists_lt_of_lt_ciSup₂'

Modification history

2026-08-22 18:51
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
feat(ConditionallyCompleteLattice/Indexed): add binary versions of lemmas (#38906) …
Added exists_lt_of_lt_ciSup₂'View on Github →