Documentation

Init.Data.Subtype.Order

instance Std.instLESubtype {α : Type u} [LE α] {P : αProp} :
Equations
instance Std.instLTSubtype {α : Type u} [LT α] {P : αProp} :
Equations
instance Std.instLawfulOrderLTSubtype {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {P : αProp} :
instance Std.instBEqSubtype {α : Type u} [BEq α] {P : αProp} :
Equations
instance Std.instMinSubtypeOfMinEqOr {α : Type u} [Min α] [MinEqOr α] {P : αProp} :
Equations
instance Std.instMaxSubtypeOfMaxEqOr_1 {α : Type u} [Max α] [MaxEqOr α] {P : αProp} :
Equations
instance Std.instReflSubtypeLe {α : Type u} [LE α] [i : Refl fun (x1 x2 : α) => x1 x2] {P : αProp} :
Refl fun (x1 x2 : Subtype P) => x1 x2
instance Std.instAntisymmSubtypeLe {α : Type u} [LE α] [i : Antisymm fun (x1 x2 : α) => x1 x2] {P : αProp} :
Antisymm fun (x1 x2 : Subtype P) => x1 x2
instance Std.instTotalSubtypeLe {α : Type u} [LE α] [i : Total fun (x1 x2 : α) => x1 x2] {P : αProp} :
Total fun (x1 x2 : Subtype P) => x1 x2
instance Std.instTransSubtypeLe {α : Type u} [LE α] [i : Trans (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {P : αProp} :
Trans (fun (x1 x2 : Subtype P) => x1 x2) (fun (x1 x2 : Subtype P) => x1 x2) fun (x1 x2 : Subtype P) => x1 x2
Equations
instance Std.instMinEqOrSubtype {α : Type u} [Min α] [MinEqOr α] {P : αProp} :
instance Std.instLawfulOrderMinSubtype {α : Type u} [LE α] [Min α] [LawfulOrderMin α] {P : αProp} :
instance Std.instMaxEqOrSubtype {α : Type u} [Max α] [MaxEqOr α] {P : αProp} :
instance Std.instLawfulOrderMaxSubtype {α : Type u} [LE α] [Max α] [LawfulOrderMax α] {P : αProp} :
instance Std.instIsPreorderSubtype {α : Type u} [LE α] [IsPreorder α] {P : αProp} :
instance Std.instIsLinearOrderSubtype {α : Type u} [LE α] [IsLinearOrder α] {P : αProp} :