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