# 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

- ULift.instLE_mathlib = { le := fun (x y : ULift.{?u.13, ?u.12} α) => x.down ≤ y.down }

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

- ULift.instLT_mathlib = { lt := fun (x y : ULift.{?u.13, ?u.12} α) => x.down < y.down }

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

- ULift.instBEq_mathlib = { beq := fun (x y : ULift.{?u.13, ?u.12} α) => x.down == y.down }

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

- ULift.instOrd_mathlib = { compare := fun (x y : ULift.{?u.13, ?u.12} α) => compare x.down y.down }

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

- ULift.instMax_mathlib = { max := fun (x y : ULift.{?u.13, ?u.12} α) => { down := x.down ⊔ y.down } }

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

- ULift.instMin_mathlib = { min := fun (x y : ULift.{?u.13, ?u.12} α) => { down := x.down ⊓ y.down } }

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

- ULift.instSDiff_mathlib = { sdiff := fun (x y : ULift.{?u.13, ?u.12} α) => { down := x.down \ y.down } }

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

- ULift.instHasCompl = { compl := fun (x : ULift.{?u.12, ?u.11} α) => { down := x.down ᶜ } }

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 : Std.OrientedOrd α] :
Std.OrientedOrd (ULift.{v, u} α)
source
instance ULift.instTransOrd_mathlib {α : Type u} [Ord α] [inst : Std.TransOrd α] :
Std.TransOrd (ULift.{v, u} α)
source
instance ULift.instLawfulBEqOrd_mathlib {α : Type u} [BEq α] [Ord α] [inst : Std.LawfulBEqOrd α] :
Std.LawfulBEqOrd (ULift.{v, u} α)
source
instance ULift.instLawfulLTOrd_mathlib {α : Type u} [LT α] [Ord α] [inst : Std.LawfulLTOrd α] :
Std.LawfulLTOrd (ULift.{v, u} α)
source
instance ULift.instLawfulLEOrd_mathlib {α : Type u} [LE α] [Ord α] [inst : Std.LawfulLEOrd α] :
Std.LawfulLEOrd (ULift.{v, u} α)
source
instance ULift.instLawfulBOrd_mathlib {α : Type u} [LE α] [LT α] [BEq α] [Ord α] [inst : Std.LawfulBOrd α] :
Std.LawfulBOrd (ULift.{v, u} α)
source
instance ULift.instPreorder {α : Type u} [Preorder α] :
Preorder (ULift.{v, u} α)
Equations

- ULift.instPreorder = Preorder.lift ULift.down

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

- ULift.instPartialOrder = PartialOrder.lift ULift.down ⋯