Documentation

Mathlib.Order.ULift

Ordered structures on ULift.{v} α #

Once these basic instances are setup, the instances of more complex typeclasses should live next to the corresponding Prod instances.

source
instance ULift.instLE_mathlib {α : Type u} [LE α] :
LE (ULift.{v, u} α)
Equations
    source
    @[simp]
    theorem ULift.up_le {α : Type u} [LE α] {a b : α} :
    { down := a } ≤ { down := b } ↔ a ≤ b
    source
    @[simp]
    theorem ULift.down_le {α : Type u} [LE α] {a b : ULift.{u_1, u} α} :
    a.down ≤ b.down ↔ a ≤ b
    source
    instance ULift.instLT_mathlib {α : Type u} [LT α] :
    LT (ULift.{v, u} α)
    Equations
      source
      @[simp]
      theorem ULift.up_lt {α : Type u} [LT α] {a b : α} :
      { down := a } < { down := b } ↔ a < b
      source
      @[simp]
      theorem ULift.down_lt {α : Type u} [LT α] {a b : ULift.{u_1, u} α} :
      a.down < b.down ↔ a < b
      source
      instance ULift.instBEq_mathlib {α : Type u} [BEq α] :
      BEq (ULift.{v, u} α)
      Equations
        source
        @[simp]
        theorem ULift.up_beq {α : Type u} [BEq α] (a b : α) :
        ({ down := a } == { down := b }) = (a == b)
        source
        @[simp]
        theorem ULift.down_beq {α : Type u} [BEq α] (a b : ULift.{u_1, u} α) :
        (a.down == b.down) = (a == b)
        source
        instance ULift.instOrd_mathlib {α : Type u} [Ord α] :
        Ord (ULift.{v, u} α)
        Equations
          source
          @[simp]
          theorem ULift.up_compare {α : Type u} [Ord α] (a b : α) :
          compare { down := a } { down := b } = compare a b
          source
          @[simp]
          theorem ULift.down_compare {α : Type u} [Ord α] (a b : ULift.{u_1, u} α) :
          compare a.down b.down = compare a b
          source
          instance ULift.instMax_mathlib {α : Type u} [Max α] :
          Max (ULift.{v, u} α)
          Equations
            source
            @[simp]
            theorem ULift.up_sup {α : Type u} [Max α] (a b : α) :
            { down := a ⊔ b } = { down := a } ⊔ { down := b }
            source
            @[simp]
            theorem ULift.down_sup {α : Type u} [Max α] (a b : ULift.{u_1, u} α) :
            (a ⊔ b).down = a.down ⊔ b.down
            source
            instance ULift.instMin_mathlib {α : Type u} [Min α] :
            Min (ULift.{v, u} α)
            Equations
              source
              @[simp]
              theorem ULift.up_inf {α : Type u} [Min α] (a b : α) :
              { down := a ⊓ b } = { down := a } ⊓ { down := b }
              source
              @[simp]
              theorem ULift.down_inf {α : Type u} [Min α] (a b : ULift.{u_1, u} α) :
              (a ⊓ b).down = a.down ⊓ b.down
              source
              instance ULift.instSDiff_mathlib {α : Type u} [SDiff α] :
              SDiff (ULift.{v, u} α)
              Equations
                source
                @[simp]
                theorem ULift.up_sdiff {α : Type u} [SDiff α] (a b : α) :
                { down := a \ b } = { down := a } \ { down := b }
                source
                @[simp]
                theorem ULift.down_sdiff {α : Type u} [SDiff α] (a b : ULift.{u_1, u} α) :
                (a \ b).down = a.down \ b.down
                source
                instance ULift.instHasCompl {α : Type u} [HasCompl α] :
                HasCompl (ULift.{v, u} α)
                Equations
                  source
                  @[simp]
                  theorem ULift.up_compl {α : Type u} [HasCompl α] (a : α) :
                  { down := aᶜ } = { down := a }ᶜ
                  source
                  @[simp]
                  theorem ULift.down_compl {α : Type u} [HasCompl α] (a : ULift.{u_1, u} α) :
                  aᶜ.down = a.downᶜ
                  source
                  instance ULift.instOrientedOrd_mathlib {α : Type u} [Ord α] [inst : Batteries.OrientedOrd α] :
                  Batteries.OrientedOrd (ULift.{v, u} α)
                  source
                  instance ULift.instTransOrd_mathlib {α : Type u} [Ord α] [inst : Batteries.TransOrd α] :
                  Batteries.TransOrd (ULift.{v, u} α)
                  source
                  instance ULift.instBEqOrd_mathlib {α : Type u} [BEq α] [Ord α] [inst : Batteries.BEqOrd α] :
                  Batteries.BEqOrd (ULift.{v, u} α)
                  source
                  instance ULift.instLTOrd_mathlib {α : Type u} [LT α] [Ord α] [inst : Batteries.LTOrd α] :
                  Batteries.LTOrd (ULift.{v, u} α)
                  source
                  instance ULift.instLEOrd_mathlib {α : Type u} [LE α] [Ord α] [inst : Batteries.LEOrd α] :
                  Batteries.LEOrd (ULift.{v, u} α)
                  source
                  instance ULift.instLawfulOrd_mathlib {α : Type u} [LE α] [LT α] [BEq α] [Ord α] [inst : Batteries.LawfulOrd α] :
                  Batteries.LawfulOrd (ULift.{v, u} α)
                  source
                  instance ULift.instPreorder {α : Type u} [Preorder α] :
                  Preorder (ULift.{v, u} α)
                  Equations
                    source
                    instance ULift.instPartialOrder {α : Type u} [PartialOrder α] :
                    PartialOrder (ULift.{v, u} α)
                    Equations