Theorems · Inductive type · order theory
IsDirected
(α : Sort u_5) → (α → α → Prop) → Prop
IsDirected α r states that for any elements a, b there exists an element c such that
r a c and r b c.
- Defined in
- Mathlib.Order.Directed
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by20
Results whose statement or proof uses this declaration.
- IsDirectedOrderproof · cited by 316
- IsCodirectedOrderproof · cited by 95
- directed_ofstatement and proof · cited by 14
- directed_idstatement and proof · cited by 7
- IsDirected.directedstatement and proof · cited by 3
- directed_id_iffstatement · cited by 2
- directedOn_iff_isCodirectedOrderproof · cited by 2
- directedOn_iff_isDirectedOrderproof · cited by 2
- directedOn_univstatement and proof · cited by 1
- directed_of₃statement and proof · cited by 1
- isDirected_onFunstatement and proof · cited by 1
- Real.isLUB_of_tendsto_monotone_bddAbovestatement and proof · cited by 0