Theorem isGLB_ciInf

Modification history

2026-08-18 15:22
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
feat(Data/Fintype/Order): add `Finite.ciInf_le_iff` and friends (#42623) …
Deleted isGLB_ciInfView on Github →
2024-10-22 14:55
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
refactor(Order/ConditionallyCompleteLattice): split large file (#18029)
Modified isGLB_ciInfView on Github →
2023-05-14 07:05
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
chore: Rename to `sSup`/`iSup` (#3938) …
Added isGLB_ciInfView on Github →