Structures · Order
IsNonstrictStrictOrder
An unbundled relation class stating that r is the nonstrict relation corresponding to the
strict relation s. Compare lt_iff_le_not_ge. This is mostly meant to provide dot
notation on (⊆) and (⊂).
- Defined in
- Mathlib.Order.RelClasses
- Shape
- 3 explicit arguments · adds right_iff_left_not_left
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every IsNonstrictStrictOrder is also a
Concrete types that are instances2
- ZFSet
- Multiset
How is a type an instance?
Loading the hierarchy index…