Structures · Lean core
Std.IsLinearPreorder
This typeclass states that the order structure on α, represented by an LE α instance,
is a linear preorder.
In other words, the less-or-equal relation is reflexive, transitive and total.
- Defined in
- Init.Data.Order.Classes
- Shape
- One type argument · adds le_total
Extends1
Extended by2
Concrete types that are instances3
- Dyadic
- Lean.Grind.IntModule.OfNatModule.Q
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by0
No theorem or definition in Mathlib takes this class as a hypothesis.