Theorems · Theorem · order theory
isLUB_Ioo
∀ {γ : Type u_3} [inst : SemilatticeInf γ] [DenselyOrdered γ] {a b : γ}, b < a → IsLUB (Set.Ioo b a) a- Defined in
- Mathlib.Order.Bounds.Basic
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemilatticeInfDenselyOrdered
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.
- LT.lt.leproof · cited by 2,189
- Set.Ioostatement and proof · cited by 1,214
- SemilatticeInfstatement and proof · cited by 634
- DenselyOrderedstatement and proof · cited by 471
- inf_le_leftproof · cited by 286
- IsLUBstatement · cited by 280
- upperBoundsproof · cited by 263
- inf_le_rightproof · cited by 238
- LE.le.trans'proof · cited by 140
- le_infproof · cited by 107
- LT.lt.trans_le'proof · cited by 52
- not_lt_of_geproof · cited by 52
Cited by7
Results whose statement or proof uses this declaration.
- closure_Iooproof · cited by 20
- exists_seq_strictMono_tendsto'proof · cited by 6
- isLUB_Icoproof · cited by 3
- Dense.exists_seq_strictMono_tendsto_of_ltproof · cited by 3
- csSup_Iooproof · cited by 1
- upperBounds_Iooproof · cited by 0
- right_nhdsWithin_Ioo_neBotproof · cited by 0