Theorem ciInf_le_ciSup

Modification history

2025-01-10 13:20
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573) …
Added ciInf_le_ciSupView on Github →