Theorems · Definition · order theory
IsCofinalFor
{α : Type u_1} → [LE α] → Set α → Set α → PropA set s is said to be cofinal for a set t if, for all a ∈ s there exists b ∈ t
such that a ≤ b.
- Defined in
- Mathlib.Order.Bounds.Defs
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 4 from the axioms · 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.
- Setstatement and proof · cited by 53,352
Cited by24
Results whose statement or proof uses this declaration.
- upperBounds_mono_of_isCofinalForstatement and proof · cited by 3
- IsCofinalFor.of_subsetstatement · cited by 3
- LE.le.isCofinalForstatement · cited by 3
- IsCofinalFor.nonemptystatement and proof · cited by 2
- IsCofinalFor.transstatement and proof · cited by 2
- IsCofinalFor.union_leftstatement and proof · cited by 2
- IsCofinalFor.union_rightstatement and proof · cited by 2
- dirSupInaccOn_iff_inter_subsetproof · cited by 2
- IsLUB.of_isCofinalForstatement and proof · cited by 2
- directedOn_union_iffstatement and proof · cited by 2
- DirectedOn.of_isCofinalForstatement and proof · cited by 2
- DirSupClosedOn.unionproof · cited by 2