Structures · Order
GradeOrder
An 𝕆-graded order is an order α equipped with a strictly monotone function
grade 𝕆 : α → 𝕆 which preserves order covering (CovBy).
- Defined in
- Mathlib.Order.Grade
- Shape
- 2 explicit arguments · adds grade, grade_strictMono, covBy_grade
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances2
- Int
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by27
- grade
- grade_strictMono
- GradeOrder.grade
- GradeOrder.grade_strictMono
- grade_injective
- CovBy.grade
- covBy_iff_lt_covBy_grade
- grade_lt_grade_iff
- GradeOrder.covBy_grade
- grade_le_grade_iff
- grade_toDual
- GradeOrder.wellFoundedLT
- grade_ne_grade_iff
- OrderDual.gradeOrder
- Flag.instGradeOrderSubtypeMem
- grade_mono
- Flag.grade_coe
- GradeOrder.liftLeft
- GradeOrder.wellFoundedGT
- GradeOrder.finToNat
- GradeOrder.natToInt
- grade_covBy_grade_iff
- GradeOrder.liftRight
- instWellFoundedGTOfGradeOrderOrderDualNat
- grade_eq_grade_iff
- instWellFoundedLTOfGradeOrderNat
- grade_ofDual
Ancestors0
No ancestors.