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.

instance ULift.instLE_mathlib {α : Type u} [LE α] :
Equations
@[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 : ULift.{u_1, u} α} {b : ULift.{u_1, u} α} :
a.down b.down a b
instance ULift.instLT_mathlib {α : Type u} [LT α] :
Equations
@[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 : ULift.{u_1, u} α} {b : ULift.{u_1, u} α} :
a.down < b.down a < b
instance ULift.instBEq_mathlib {α : Type u} [BEq α] :
Equations
@[simp]
theorem ULift.up_beq {α : Type u} [BEq α] (a : α) (b : α) :
({ down := a } == { down := b }) = (a == b)
@[simp]
theorem ULift.down_beq {α : Type u} [BEq α] (a : ULift.{u_1, u} α) (b : ULift.{u_1, u} α) :
(a.down == b.down) = (a == b)
instance ULift.instOrd_mathlib {α : Type u} [Ord α] :
Equations
@[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 : ULift.{u_1, u} α) (b : ULift.{u_1, u} α) :
compare a.down b.down = compare a b
instance ULift.instSup {α : Type u} [Sup α] :
Equations
@[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 : ULift.{u_1, u} α) (b : ULift.{u_1, u} α) :
(a b).down = a.down b.down
instance ULift.instInf {α : Type u} [Inf α] :
Equations
@[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 : ULift.{u_1, u} α) (b : ULift.{u_1, u} α) :
(a b).down = a.down b.down
instance ULift.instSDiff_mathlib {α : Type u} [SDiff α] :
Equations
@[simp]
theorem ULift.up_sdiff {α : Type u} [SDiff α] (a : α) (b : α) :
{ down := a \ b } = { down := a } \ { down := b }
@[simp]
theorem ULift.down_sdiff {α : Type u} [SDiff α] (a : ULift.{u_1, u} α) (b : ULift.{u_1, u} α) :
(a \ b).down = a.down \ b.down
Equations
@[simp]
theorem ULift.up_compl {α : Type u} [HasCompl α] (a : α) :
{ down := a } = { down := a }
@[simp]
theorem ULift.down_compl {α : Type u} [HasCompl α] (a : ULift.{u_1, u} α) :
a.down = a.down
Equations
  • =
instance ULift.instBEqOrd_mathlib {α : Type u} [BEq α] [Ord α] [inst : Batteries.BEqOrd α] :
Equations
  • =
instance ULift.instLTOrd_mathlib {α : Type u} [LT α] [Ord α] [inst : Batteries.LTOrd α] :
Equations
  • =
instance ULift.instLEOrd_mathlib {α : Type u} [LE α] [Ord α] [inst : Batteries.LEOrd α] :
Equations
  • =
instance ULift.instLawfulOrd_mathlib {α : Type u} [LE α] [LT α] [BEq α] [Ord α] [inst : Batteries.LawfulOrd α] :
Equations
  • =
Equations
Equations