Documentation

Init.Data.Subtype.Order

source
instance Subtype.instLE {α : Type u} [LE α] {P : α → Prop} :
LE (Subtype P)
Equations
    source
    instance Subtype.instLT {α : Type u} [LT α] {P : α → Prop} :
    LT (Subtype P)
    Equations
      source
      instance Subtype.instLawfulOrderLT {α : Type u} [LT α] [LE α] [Std.LawfulOrderLT α] {P : α → Prop} :
      Std.LawfulOrderLT (Subtype P)
      source
      instance Subtype.instMin {α : Type u} [Min α] [Std.MinEqOr α] {P : α → Prop} :
      Min (Subtype P)
      Equations
        source
        instance Subtype.instMax {α : Type u} [Max α] [Std.MaxEqOr α] {P : α → Prop} :
        Max (Subtype P)
        Equations
          source
          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
          source
          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
          source
          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
          source
          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
            source
            instance Subtype.instMinEqOr {α : Type u} [Min α] [Std.MinEqOr α] {P : α → Prop} :
            Std.MinEqOr (Subtype P)
            source
            instance Subtype.instLawfulOrderMin {α : Type u} [LE α] [Min α] [Std.LawfulOrderMin α] {P : α → Prop} :
            Std.LawfulOrderMin (Subtype P)
            source
            instance Subtype.instMaxEqOr {α : Type u} [Max α] [Std.MaxEqOr α] {P : α → Prop} :
            Std.MaxEqOr (Subtype P)
            source
            instance Subtype.instLawfulOrderMax {α : Type u} [LE α] [Max α] [Std.LawfulOrderMax α] {P : α → Prop} :
            Std.LawfulOrderMax (Subtype P)
            source
            instance Subtype.instIsPreorder {α : Type u} [LE α] [Std.IsPreorder α] {P : α → Prop} :
            Std.IsPreorder (Subtype P)
            source
            instance Subtype.instIsLinearPreorder {α : Type u} [LE α] [Std.IsLinearPreorder α] {P : α → Prop} :
            Std.IsLinearPreorder (Subtype P)
            source
            instance Subtype.instIsPartialOrder {α : Type u} [LE α] [Std.IsPartialOrder α] {P : α → Prop} :
            Std.IsPartialOrder (Subtype P)
            source
            instance Subtype.instIsLinearOrder {α : Type u} [LE α] [Std.IsLinearOrder α] {P : α → Prop} :
            Std.IsLinearOrder (Subtype P)