Theorems · Definition · order theory
IsCodirectedOrder
(α : Type u_5) → [LE α] → Prop
A class for an IsDirected relation ≥.
- Defined in
- Mathlib.Order.Directed
- Cited by
- 95 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 4 definitions · uses no axioms
- Assumes
- LE
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsDirectedproof · cited by 16
Cited by96
Results whose statement or proof uses this declaration.
- Filter.atBot_basisstatement and proof · cited by 14
- Filter.mem_atBot_setsstatement and proof · cited by 10
- exists_le_lestatement and proof · cited by 9
- Set.Finite.bddBelowstatement and proof · cited by 7
- Monotone.le_of_tendstostatement and proof · cited by 4
- Monotone.measure_iInterstatement and proof · cited by 4
- Filter.eventually_atBotstatement and proof · cited by 4
- IsMin.isBotstatement and proof · cited by 4
- Monotone.directed_gestatement and proof · cited by 3
- iInf_iSup_of_monotonestatement and proof · cited by 3
- iInf_sup_of_monotonestatement and proof · cited by 3
- Filter.atBot_basis_Iiostatement and proof · cited by 3