Theorems · Inductive type · order theory
Order.IsPredLimit
{α : Type u_1} → [Preorder α] → α → PropA predecessor limit is a value that isn't maximal and isn't covered by any other.
It's so named because in a predecessor order, a predecessor limit can't be the predecessor of
anything larger.
Use IsPredPrelimit if you want to include the case of a maximal element.
- Defined in
- Mathlib.Order.SuccPred.Limit
- Cited by
- 60 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Preorder
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.
- Preorderstatement · cited by 7,952
Cited by64
Results whose statement or proof uses this declaration.
- Order.IsPredLimit.isPredPrelimitstatement and proof · cited by 23
- Order.IsPredLimit.not_isMaxstatement and proof · cited by 11
- Order.isPredLimit_iffstatement and proof · cited by 10
- PredOrder.colimitRecOnstatement and proof · cited by 4
- Order.isPredLimitRecOnstatement and proof · cited by 4
- csInf_mem_of_not_isPredLimitstatement and proof · cited by 3
- IsGLB.mem_of_nonempty_of_not_isPredLimitstatement and proof · cited by 2
- PredOrder.isOpen_singleton_iffstatement and proof · cited by 2
- PredOrder.nhds_eq_purestatement · cited by 2
- Order.isPredPrelimit_iff_isPredLimitstatement · cited by 1
- Order.isPredPrelimit_iff_isPredLimit_of_not_isMaxstatement · cited by 1
- Order.isSuccLimit_toDual_iffstatement · cited by 1