instance
Std.instLawfulOrderLTSubtype
{α : Type u}
[LT α]
[LE α]
[LawfulOrderLT α]
{P : α → Prop}
:
LawfulOrderLT (Subtype P)
instance
Std.instLawfulOrderMinSubtype
{α : Type u}
[LE α]
[Min α]
[LawfulOrderMin α]
{P : α → Prop}
:
instance
Std.instLawfulOrderMaxSubtype
{α : Type u}
[LE α]
[Max α]
[LawfulOrderMax α]
{P : α → Prop}
:
instance
Std.instIsPreorderSubtype
{α : Type u}
[LE α]
[IsPreorder α]
{P : α → Prop}
:
IsPreorder (Subtype P)
instance
Std.instIsLinearOrderSubtype
{α : Type u}
[LE α]
[IsLinearOrder α]
{P : α → Prop}
:
IsLinearOrder (Subtype P)