Theorems · Theorem · order theory
Directed.finite_le
∀ {α : Type u_2} {r : α → α → Prop} [IsTrans α r] {ι : Sort u_4} {κ : Sort u_5} [Nonempty ι] [Finite κ] {f : ι → α},
Directed r f → ∀ (g : κ → ι), ∃ z, ∀ (i : κ), r (f (g i)) (f z)- Defined in
- Mathlib.Data.Fintype.Order
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finitestatement and proof · cited by 3,029
- Directedstatement and proof · cited by 213
- IsTransstatement and proof · cited by 157
- Set.finite_rangeproof · cited by 58
- PLift.down_surjectiveproof · cited by 4
- Directed.finite_set_leproof · cited by 3
- Directed.comp_of_surjectiveproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- Finite.exists_leproof · cited by 4
- le_iSup_iff_of_directedproof · cited by 2
- FirstOrder.Language.Substructure.mem_iSup_of_directedproof · cited by 1
- IntermediateField.Lifts.union_isExtendibleproof · cited by 1
- Finite.exists_geproof · cited by 1