Structures · Order
GradeMaxOrder
An 𝕆-graded order where maximal elements have maximal grades.
- Defined in
- Mathlib.Order.Grade
- Shape
- 2 explicit arguments · adds isMax_grade
Extends1
Extended by1
Concrete types that are instances1
- OrderDual
How is a type an instance?
Loading the hierarchy index…