Theorems · Definition · order theory
Directed
{α : Type u_1} → {ι : Sort u_3} → (α → α → Prop) → (ι → α) → PropA family of elements of α is directed (with respect to a relation ≼ on α)
if there is a member of the family ≼-above any pair in the family.
- Defined in
- Mathlib.Order.Directed
- Cited by
- 213 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · 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 by218
Results whose statement or proof uses this declaration.
- DirectedOn.directed_valstatement · cited by 36
- Monotone.directed_lestatement · cited by 25
- Directed.directedOn_rangestatement · cited by 17
- directedOn_iff_directedstatement · cited by 14
- Directed.mono_compstatement and proof · cited by 12
- IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosedstatement and proof · cited by 11
- Directed.sequencestatement and proof · cited by 10
- Filter.mem_iInf_of_directedstatement and proof · cited by 9
- directed_compstatement · cited by 8
- directed_of_isDirected_lestatement · cited by 8
- Submodule.mem_iSup_of_directedstatement and proof · cited by 7
- directed_idstatement · cited by 7
Showing the 200 most cited of 218.