Structures · Order
IsStrictTotalOrder
IsStrictTotalOrder X lt means that the binary relation lt on X is a strict total order,
that is, Std.Trichotomous lt and IsStrictOrder X lt.
- Defined in
- Mathlib.Order.Defs.Unbundled
- Shape
- 2 explicit arguments
Extends2
Extended by1
Forgetful instances
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- linearOrderOfSTO
- Pi.Lex.wellFounded
- Concept.isCompl_extent_intent
- RelEmbedding.isStrictTotalOrder
- Finsupp.Lex.wellFounded_of_finite
- Concept.compl_intent
- Function.instIsStrictTotalOrderSwapProp
- Function.Injective.isStrictTotalOrder_onFun
- IsStrictTotalOrder.toIsStrictOrder
- Concept.compl_extent
- isStrictOrderConnected_of_isStrictTotalOrder
- IsStrictTotalOrder.swap
- IsStrictTotalOrder.toTrichotomous
- DFinsupp.Lex.wellFounded_of_finite