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.

@[implicit_reducible]

instance ULift.instLE_mathlib {α : Type u} [LE α] : LE (ULift.{v, u} α)

@[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 : ULift.{u_1, u} α} : a.down ≤ b.down ↔ a ≤ b

@[implicit_reducible]

instance ULift.instLT_mathlib {α : Type u} [LT α] : LT (ULift.{v, u} α)

@[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 : ULift.{u_1, u} α} : a.down < b.down ↔ a < b

@[implicit_reducible]

instance ULift.instBEq_mathlib {α : Type u} [BEq α] : BEq (ULift.{v, u} α)

@[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 b : ULift.{u_1, u} α) : (a.down == b.down) = (a == b)

@[implicit_reducible]

instance ULift.instOrd_mathlib {α : Type u} [Ord α] : Ord (ULift.{v, u} α)

@[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 : ULift.{u_1, u} α) : compare a.down b.down = compare a b

@[implicit_reducible]

instance ULift.instMax_mathlib {α : Type u} [Max α] : Max (ULift.{v, u} α)

@[implicit_reducible]

instance ULift.instMin_mathlib {α : Type u} [Min α] : Min (ULift.{v, u} α)

@[simp]

theorem ULift.up_sup {α : Type u} [Max α] (a b : α) : { down := a ⊔ b } = { down := a } ⊔ { down := b }

@[simp]

theorem ULift.up_inf {α : Type u} [Min α] (a b : α) : { down := a ⊓ b } = { down := a } ⊓ { down := b }

@[simp]

theorem ULift.down_sup {α : Type u} [Max α] (a b : ULift.{u_1, u} α) : (a ⊔ b).down = a.down ⊔ b.down

@[simp]

theorem ULift.down_inf {α : Type u} [Min α] (a b : ULift.{u_1, u} α) : (a ⊓ b).down = a.down ⊓ b.down

@[implicit_reducible]

instance ULift.instSDiff_mathlib {α : Type u} [SDiff α] : SDiff (ULift.{v, u} α)

@[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 b : ULift.{u_1, u} α) : (a \ b).down = a.down \ b.down

@[implicit_reducible]

instance ULift.instCompl {α : Type u} [Compl α] : Compl (ULift.{v, u} α)

@[simp]

theorem ULift.up_compl {α : Type u} [Compl α] (a : α) : { down := aᶜ } = { down := a }ᶜ

@[simp]

theorem ULift.down_compl {α : Type u} [Compl α] (a : ULift.{u_1, u} α) : aᶜ.down = a.downᶜ

instance ULift.instOrientedOrd_mathlib {α : Type u} [Ord α] [inst : Std.OrientedOrd α] : Std.OrientedOrd (ULift.{v, u} α)

instance ULift.instTransOrd_mathlib {α : Type u} [Ord α] [inst : Std.TransOrd α] : Std.TransOrd (ULift.{v, u} α)

instance ULift.instLawfulBEqOrd_mathlib {α : Type u} [BEq α] [Ord α] [inst : Std.LawfulBEqOrd α] : Std.LawfulBEqOrd (ULift.{v, u} α)

instance ULift.instLawfulLTOrd_mathlib {α : Type u} [LT α] [Ord α] [inst : Std.LawfulLTOrd α] : Std.LawfulLTOrd (ULift.{v, u} α)

instance ULift.instLawfulLEOrd_mathlib {α : Type u} [LE α] [Ord α] [inst : Std.LawfulLEOrd α] : Std.LawfulLEOrd (ULift.{v, u} α)

instance ULift.instLawfulBOrd_mathlib {α : Type u} [LE α] [LT α] [BEq α] [Ord α] [inst : Std.LawfulBOrd α] : Std.LawfulBOrd (ULift.{v, u} α)

@[implicit_reducible]

instance ULift.instPreorder {α : Type u} [Preorder α] : Preorder (ULift.{v, u} α)

@[implicit_reducible]

instance ULift.instPartialOrder {α : Type u} [PartialOrder α] : PartialOrder (ULift.{v, u} α)