Theorems · Theorem · order theory
isGLB_Ioo
∀ {γ : Type u_3} [inst : SemilatticeSup γ] [DenselyOrdered γ] {a b : γ}, a < b → IsGLB (Set.Ioo a b) a- Defined in
- Mathlib.Order.Bounds.Basic
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemilatticeSupDenselyOrdered
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LE.le.transproof · cited by 3,151
- LT.lt.leproof · cited by 2,189
- Set.Ioostatement and proof · cited by 1,214
- SemilatticeSupstatement and proof · cited by 785
- LT.lt.trans_leproof · cited by 678
- DenselyOrderedstatement and proof · cited by 471
- le_sup_leftproof · cited by 265
- le_sup_rightproof · cited by 242
- IsGLBstatement · cited by 213
- lowerBoundsproof · cited by 212
- sup_leproof · cited by 159
- exists_betweenproof · cited by 102
Cited by5
Results whose statement or proof uses this declaration.
- closure_Iooproof · cited by 20
- csInf_Iooproof · cited by 4
- isGLB_Iocproof · cited by 3
- lowerBounds_Iooproof · cited by 0
- left_nhdsWithin_Ioo_neBotproof · cited by 0