@[instance_reducible]

instance Subtype.instLE {α : Type u} [LE α] {P : α → Prop} : LE (Subtype P)

Equations

• Subtype.instLE = { le := fun (a b : Subtype P) => a.val ≤ b.val }

@[instance_reducible]

instance Subtype.instLT {α : Type u} [LT α] {P : α → Prop} : LT (Subtype P)

Equations

• Subtype.instLT = { lt := fun (a b : Subtype P) => a.val < b.val }

instance Subtype.instLawfulOrderLT {α : Type u} [LT α] [LE α] [Std.LawfulOrderLT α] {P : α → Prop} : Std.LawfulOrderLT (Subtype P)

@[instance_reducible]

instance Subtype.instMin {α : Type u} [Min α] [Std.MinEqOr α] {P : α → Prop} : Min (Subtype P)

Equations

• Subtype.instMin = { min := fun (a b : Subtype P) => ⟨min a.val b.val, ⋯⟩ }

@[instance_reducible]

instance Subtype.instMax {α : Type u} [Max α] [Std.MaxEqOr α] {P : α → Prop} : Max (Subtype P)

Equations

• Subtype.instMax = { max := fun (a b : Subtype P) => ⟨max a.val b.val, ⋯⟩ }

instance Subtype.instReflLE {α : Type u} [LE α] [i : Std.Refl fun (x1 x2 : α) => x1 ≤ x2] {P : α → Prop} : Std.Refl fun (x1 x2 : Subtype P) => x1 ≤ x2

instance Subtype.instAntisymmLE {α : Type u} [LE α] [i : Std.Antisymm fun (x1 x2 : α) => x1 ≤ x2] {P : α → Prop} : Std.Antisymm fun (x1 x2 : Subtype P) => x1 ≤ x2

instance Subtype.instTotalLE {α : Type u} [LE α] [i : Std.Total fun (x1 x2 : α) => x1 ≤ x2] {P : α → Prop} : Std.Total fun (x1 x2 : Subtype P) => x1 ≤ x2

@[instance_reducible]

instance Subtype.instTransLE {α : 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

• Subtype.instTransLE = { trans := ⋯ }

instance Subtype.instMinEqOr {α : Type u} [Min α] [Std.MinEqOr α] {P : α → Prop} : Std.MinEqOr (Subtype P)

instance Subtype.instLawfulOrderMin {α : Type u} [LE α] [Min α] [Std.LawfulOrderMin α] {P : α → Prop} : Std.LawfulOrderMin (Subtype P)

instance Subtype.instMaxEqOr {α : Type u} [Max α] [Std.MaxEqOr α] {P : α → Prop} : Std.MaxEqOr (Subtype P)

instance Subtype.instLawfulOrderMax {α : Type u} [LE α] [Max α] [Std.LawfulOrderMax α] {P : α → Prop} : Std.LawfulOrderMax (Subtype P)

instance Subtype.instIsPreorder {α : Type u} [LE α] [Std.IsPreorder α] {P : α → Prop} : Std.IsPreorder (Subtype P)

instance Subtype.instIsLinearPreorder {α : Type u} [LE α] [Std.IsLinearPreorder α] {P : α → Prop} : Std.IsLinearPreorder (Subtype P)

instance Subtype.instIsPartialOrder {α : Type u} [LE α] [Std.IsPartialOrder α] {P : α → Prop} : Std.IsPartialOrder (Subtype P)

instance Subtype.instIsLinearOrder {α : Type u} [LE α] [Std.IsLinearOrder α] {P : α → Prop} : Std.IsLinearOrder (Subtype P)