Structures · Lean core
Std.LawfulOrderBEq
This class has no docstring in Mathlib.
- Defined in
- Init.Data.Order.Classes
- Shape
- One type argument · adds beq_iff_le_and_ge
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances3
- String.Pos.Raw
- String.Slice.Pos
- String.Pos
How is a type an instance?
Loading the hierarchy index…
Assumed by0
No theorem or definition in Mathlib takes this class as a hypothesis.
Ancestors0
No ancestors.