Theorems · Theorem · order theory
directed_of
∀ {α : Type u_1} (r : α → α → Prop) [IsDirected α r] (a b : α), ∃ c, r a c ∧ r b c- Defined in
- Mathlib.Order.Directed
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- IsDirected
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.
- IsDirectedstatement and proof · cited by 16
- IsDirected.directedproof · cited by 3
Cited by14
Results whose statement or proof uses this declaration.
- exists_ge_geproof · cited by 22
- exists_le_leproof · cited by 9
- directed_idproof · cited by 7
- iSup_inf_of_monotoneproof · cited by 3
- FirstOrder.Language.DirectLimit.equiv_iffproof · cited by 3
- iInf_sup_of_monotoneproof · cited by 3
- UniformOnFun.hasAntitoneBasis_uniformityproof · cited by 2
- FirstOrder.Language.DirectLimit.funMap_unify_equivproof · cited by 1
- directedOn_univproof · cited by 1
- directed_of₃proof · cited by 1
- FirstOrder.Language.DirectLimit.relMap_unify_equivproof · cited by 1
- FirstOrder.Language.DirectLimit.funMap_quotient_mk'_sigma_mk'proof · cited by 0