Structures · Order
IsDirected
IsDirected α r states that for any elements a, b there exists an element c such that
r a c and r b c.
- Defined in
- Mathlib.Order.Directed
- Shape
- 2 explicit arguments · adds directed
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- Finset
How is a type an instance?
Loading the hierarchy index…
Assumed by10
Ancestors0
No ancestors.