Commit 2026-03-23 02:33 7573b3f6
View on Github →feat(Order/ConditionallyCompleteLattice/Indexed): f i j ≤ ⨆ (i) (j), f i j (#36168)
Add le_ciSup₂/ciInf₂_le to match CompleteLattice's le_iSup₂/iInf₂_le.
feat(Order/ConditionallyCompleteLattice/Indexed): f i j ≤ ⨆ (i) (j), f i j (#36168)
Add le_ciSup₂/ciInf₂_le to match CompleteLattice's le_iSup₂/iInf₂_le.