Documentation

Init.Data.Subtype.Order

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

Equations

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

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

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 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 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 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)