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