Theorems · Theorem · order theory
exists_ge_ge
∀ {α : Type u_1} [inst : LE α] [IsDirectedOrder α] (a b : α), ∃ c, a ≤ c ∧ b ≤ c- Defined in
- Mathlib.Order.Directed
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- LEIsDirectedOrder
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.
- IsDirectedOrderstatement and proof · cited by 316
- directed_ofproof · cited by 14
Cited by22
Results whose statement or proof uses this declaration.
- DirectLimit.map₀_defproof · cited by 7
- IsMax.isTopproof · cited by 4
- Filter.exists_seq_monotone_tendsto_atTop_atTopproof · cited by 3
- Filter.atTop_basis'proof · cited by 3
- Filter.map_atTop_eq_of_gc_preorderproof · cited by 3
- Filter.map_val_atTop_of_Ici_subsetproof · cited by 3
- Module.DirectLimit.exists_ofproof · cited by 3
- Filter.atTop_basis_Ioi'proof · cited by 2
- BddAbove.unionproof · cited by 2
- Ring.DirectLimit.exists_ofproof · cited by 2
- Monotone.forall_le_of_antitoneproof · cited by 2
- QuasiconvexOn.convexproof · cited by 2