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.instLEULift {α : Type u} [LE α] :
LE (ULift.{v, u} α)
Equations
  • ULift.instLEULift = { le := fun x y => 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 : ULift.{u_1, u} α} {b : ULift.{u_1, u} α} :
a.down ≤ b.down ↔ a ≤ b
source
instance ULift.instLTULift {α : Type u} [LT α] :
LT (ULift.{v, u} α)
Equations
  • ULift.instLTULift = { lt := fun x y => 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 : ULift.{u_1, u} α} {b : ULift.{u_1, u} α} :
a.down < b.down ↔ a < b
source
instance ULift.instOrdULift {α : Type u} [Ord α] :
Ord (ULift.{v, u} α)
Equations
  • ULift.instOrdULift = { compare := fun x y => 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 : ULift.{u_1, u} α) (b : ULift.{u_1, u} α) :
compare a.down b.down = compare a b
source
instance ULift.instSupULift {α : Type u} [Sup α] :
Sup (ULift.{v, u} α)
Equations
  • ULift.instSupULift = { sup := fun x y => { down := x.down ⊔ y.down } }
source
@[simp]
theorem ULift.up_sup {α : Type u} [Sup α] (a : α) (b : α) :
{ down := a ⊔ b } = { down := a } ⊔ { down := b }
source
@[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
source
instance ULift.instInfULift {α : Type u} [Inf α] :
Inf (ULift.{v, u} α)
Equations
  • ULift.instInfULift = { inf := fun x y => { down := x.down ⊓ y.down } }
source
@[simp]
theorem ULift.up_inf {α : Type u} [Inf α] (a : α) (b : α) :
{ down := a ⊓ b } = { down := a } ⊓ { down := b }
source
@[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
source
instance ULift.instSDiffULift {α : Type u} [SDiff α] :
SDiff (ULift.{v, u} α)
Equations
  • ULift.instSDiffULift = { sdiff := fun x y => { 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 : ULift.{u_1, u} α) (b : ULift.{u_1, u} α) :
(a \ b).down = a.down \ b.down
source
instance ULift.instHasComplULift {α : Type u} [HasCompl α] :
HasCompl (ULift.{v, u} α)
Equations
  • ULift.instHasComplULift = { compl := fun x => { 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.instPreorderULift {α : Type u} [Preorder α] :
Preorder (ULift.{v, u} α)
Equations
source
instance ULift.instPartialOrderULift {α : Type u} [PartialOrder α] :
PartialOrder (ULift.{v, u} α)
Equations