Theorems · Theorem · order theory
exists_le_le
∀ {α : Type u_1} [inst : LE α] [IsCodirectedOrder α] (a b : α), ∃ c ≤ a, c ≤ b- Defined in
- Mathlib.Order.Directed
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- LEIsCodirectedOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsCodirectedOrderstatement and proof · cited by 95
- directed_ofproof · cited by 14
Cited by9
Results whose statement or proof uses this declaration.
- IsMin.isBotproof · cited by 4
- Filter.map_val_atBot_of_Iic_subsetproof · cited by 3
- Filter.map_atBot_eq_of_gc_preorderproof · cited by 2
- BddBelow.unionproof · cited by 1
- Filter.atBot_basis_Iio'proof · cited by 1
- ENNReal.iInf_add_iInf_of_monotoneproof · cited by 0
- Filter.atBot_basis'proof · cited by 0
- ENat.iInf_add_iInf_of_monotoneproof · cited by 0
- Order.Ideal.inter_nonemptyproof · cited by 0