# 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.

instance ULift.instLEULift {α : Type u} [LE α] :
LE ()
Equations
• ULift.instLEULift = { le := fun (x y : ) => x.down y.down }
@[simp]
theorem ULift.up_le {α : Type u} [LE α] {a : α} {b : α} :
{ down := a } { down := b } a b
@[simp]
theorem ULift.down_le {α : Type u} [LE α] {a : } {b : } :
a.down b.down a b
instance ULift.instLTULift {α : Type u} [LT α] :
LT ()
Equations
• ULift.instLTULift = { lt := fun (x y : ) => x.down < y.down }
@[simp]
theorem ULift.up_lt {α : Type u} [LT α] {a : α} {b : α} :
{ down := a } < { down := b } a < b
@[simp]
theorem ULift.down_lt {α : Type u} [LT α] {a : } {b : } :
a.down < b.down a < b
instance ULift.instOrdULift {α : Type u} [Ord α] :
Ord ()
Equations
• ULift.instOrdULift = { compare := fun (x y : ) => compare x.down y.down }
@[simp]
theorem ULift.up_compare {α : Type u} [Ord α] (a : α) (b : α) :
compare { down := a } { down := b } = compare a b
@[simp]
theorem ULift.down_compare {α : Type u} [Ord α] (a : ) (b : ) :
compare a.down b.down = compare a b
instance ULift.instSupULift {α : Type u} [Sup α] :
Sup ()
Equations
• ULift.instSupULift = { sup := fun (x y : ) => { down := x.down y.down } }
@[simp]
theorem ULift.up_sup {α : Type u} [Sup α] (a : α) (b : α) :
{ down := a b } = { down := a } { down := b }
@[simp]
theorem ULift.down_sup {α : Type u} [Sup α] (a : ) (b : ) :
(a b).down = a.down b.down
instance ULift.instInfULift {α : Type u} [Inf α] :
Inf ()
Equations
• ULift.instInfULift = { inf := fun (x y : ) => { down := x.down y.down } }
@[simp]
theorem ULift.up_inf {α : Type u} [Inf α] (a : α) (b : α) :
{ down := a b } = { down := a } { down := b }
@[simp]
theorem ULift.down_inf {α : Type u} [Inf α] (a : ) (b : ) :
(a b).down = a.down b.down
instance ULift.instSDiffULift {α : Type u} [] :
Equations
• ULift.instSDiffULift = { sdiff := fun (x y : ) => { down := x.down \ y.down } }
@[simp]
theorem ULift.up_sdiff {α : Type u} [] (a : α) (b : α) :
{ down := a \ b } = { down := a } \ { down := b }
@[simp]
theorem ULift.down_sdiff {α : Type u} [] (a : ) (b : ) :
(a \ b).down = a.down \ b.down
instance ULift.instHasComplULift {α : Type u} [] :
Equations
• ULift.instHasComplULift = { compl := fun (x : ) => { down := x.down } }
@[simp]
theorem ULift.up_compl {α : Type u} [] (a : α) :
{ down := a } = { down := a }
@[simp]
theorem ULift.down_compl {α : Type u} [] (a : ) :
a.down = a.down
instance ULift.instPreorderULift {α : Type u} [] :
Equations
Equations