Structures · Lean core
Std.MaxEqOr
This typeclass states that Max.max a b returns one of its arguments, either a or b.
- Defined in
- Init.Data.Order.Classes
- Shape
- One type argument · adds max_eq_or
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- 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.
Ancestors0
No ancestors.