Mathlib.Order.ULift

ULift.instLE_mathlib instance

[LE α] : LE (ULift.{v} α)

Full source

instance [LE α] : LE (ULift.{v} α) where le x y := x.down ≤ y.down

Preorder Structure on Lifted Types

Informal description

For any type $\alpha$ equipped with a preorder (via the `LE` typeclass), the lifted type `ULift.{v} α` inherits a preorder structure where $a \leq b$ in `ULift.{v} α$ if and only if the corresponding elements satisfy $a \leq b$ in $\alpha$.

ULift.up_le theorem

[LE α] {a b : α} : up a ≤ up b ↔ a ≤ b

Full source

@[simp] theorem up_le [LE α] {a b : α} : upup a ≤ up b ↔ a ≤ b := Iff.rfl

Lifted Preorder Preservation: $\mathrm{up}\,a \leq \mathrm{up}\,b \leftrightarrow a \leq b$

Informal description

For any type $\alpha$ equipped with a preorder (via the `LE` typeclass), and for any elements $a, b \in \alpha$, the lifted elements $\mathrm{up}\,a$ and $\mathrm{up}\,b$ in $\mathrm{ULift}\,\alpha$ satisfy $\mathrm{up}\,a \leq \mathrm{up}\,b$ if and only if $a \leq b$ in $\alpha$.

ULift.down_le theorem

[LE α] {a b : ULift α} : down a ≤ down b ↔ a ≤ b

Full source

@[simp] theorem down_le [LE α] {a b : ULift α} : downdown a ≤ down b ↔ a ≤ b := Iff.rfl

Inequality Preservation Under Downcasting in Lifted Types

Informal description

For any type $\alpha$ equipped with a preorder (via the `LE` typeclass) and elements $a, b$ in the lifted type `ULift α`, the inequality $\mathrm{down}(a) \leq \mathrm{down}(b)$ holds in $\alpha$ if and only if $a \leq b$ holds in `ULift α`.

ULift.instLT_mathlib instance

[LT α] : LT (ULift.{v} α)

Full source

instance [LT α] : LT (ULift.{v} α) where lt x y := x.down < y.down

Strict Order on Lifted Types

Informal description

For any type $\alpha$ equipped with a strict order relation $<$, the lifted type $\mathrm{ULift}\,\alpha$ also inherits a strict order relation.

ULift.up_lt theorem

[LT α] {a b : α} : up a < up b ↔ a < b

Full source

@[simp] theorem up_lt [LT α] {a b : α} : upup a < up b ↔ a < b := Iff.rfl

Strict Order Preservation Under Lifting: $\mathrm{up}(a) < \mathrm{up}(b) \leftrightarrow a < b$

Informal description

For any type $\alpha$ equipped with a strict order relation $<$ and elements $a, b \in \alpha$, the lifted elements $\mathrm{up}(a) < \mathrm{up}(b)$ in $\mathrm{ULift}\,\alpha$ if and only if $a < b$ in $\alpha$.

ULift.down_lt theorem

[LT α] {a b : ULift α} : down a < down b ↔ a < b

Full source

@[simp] theorem down_lt [LT α] {a b : ULift α} : downdown a < down b ↔ a < b := Iff.rfl

Inequality Preservation under Downcasting in Lifted Types

Informal description

For any type $\alpha$ equipped with a strict order relation $<$ and for any elements $a, b$ in the lifted type $\mathrm{ULift}\,\alpha$, the inequality $\mathrm{down}(a) < \mathrm{down}(b)$ holds if and only if $a < b$ holds in $\mathrm{ULift}\,\alpha$.

ULift.instBEq_mathlib instance

[BEq α] : BEq (ULift.{v} α)

Full source

instance [BEq α] : BEq (ULift.{v} α) where beq x y := x.down == y.down

Boolean Equality on Lifted Types

Informal description

For any type $\alpha$ equipped with a boolean equality relation, the lifted type $\text{ULift} \alpha$ also has a boolean equality relation, where two lifted elements are equal if and only if their underlying elements are equal.

ULift.up_beq theorem

[BEq α] (a b : α) : (up a == up b) = (a == b)

Full source

@[simp] theorem up_beq [BEq α] (a b : α) : (up a == up b) = (a == b) := rfl

Preservation of Boolean Equality under Lifting

Informal description

For any type $\alpha$ with a boolean equality relation and any elements $a, b \in \alpha$, the boolean equality of the lifted elements $\text{up}(a)$ and $\text{up}(b)$ in $\text{ULift} \alpha$ is equivalent to the boolean equality of $a$ and $b$ in $\alpha$, i.e., $\text{up}(a) == \text{up}(b) = (a == b)$.

ULift.down_beq theorem

[BEq α] (a b : ULift α) : (down a == down b) = (a == b)

Full source

@[simp] theorem down_beq [BEq α] (a b : ULift α) : (down a == down b) = (a == b) := rfl

Preservation of Boolean Equality under Downcasting in Lifted Types

Informal description

For any type $\alpha$ with a boolean equality relation and for any two elements $a, b$ in the lifted type $\text{ULift} \alpha$, the boolean equality of their underlying elements $\text{down}(a)$ and $\text{down}(b)$ is equal to the boolean equality of $a$ and $b$ in $\text{ULift} \alpha$.

ULift.instOrd_mathlib instance

[Ord α] : Ord (ULift.{v} α)

Full source

instance [Ord α] : Ord (ULift.{v} α) where compare x y := compare x.down y.down

Order Structure on Lifted Types

Informal description

For any type $\alpha$ with an order structure (given by `Ord α`), the lifted type `ULift.{v} α` inherits an order structure where the ordering is preserved under the lifting operation.

ULift.up_compare theorem

[Ord α] (a b : α) : compare (up a) (up b) = compare a b

Full source

@[simp] theorem up_compare [Ord α] (a b : α) : compare (up a) (up b) = compare a b := rfl

Comparison Preservation under Lifting: $\mathrm{compare}(\mathrm{up}(a), \mathrm{up}(b)) = \mathrm{compare}(a, b)$

Informal description

For any type $\alpha$ with an order structure, and for any elements $a, b \in \alpha$, the comparison of their lifted counterparts $\mathrm{up}(a)$ and $\mathrm{up}(b)$ in $\mathrm{ULift}.\alpha$ is equal to the comparison of $a$ and $b$ in $\alpha$. That is, $\mathrm{compare}(\mathrm{up}(a), \mathrm{up}(b)) = \mathrm{compare}(a, b)$.

ULift.down_compare theorem

[Ord α] (a b : ULift α) : compare (down a) (down b) = compare a b

Full source

@[simp] theorem down_compare [Ord α] (a b : ULift α) :
  compare (down a) (down b) = compare a b := rfl

Comparison Preservation Under Lifting: $\mathrm{compare}(\mathrm{down}(a), \mathrm{down}(b)) = \mathrm{compare}(a, b)$

Informal description

For any type $\alpha$ with an order structure, and for any two elements $a, b$ in the lifted type $\mathrm{ULift}.\alpha$, the comparison of their underlying elements (via `down`) is equal to the comparison of the lifted elements themselves. That is, $\mathrm{compare}(\mathrm{down}(a), \mathrm{down}(b)) = \mathrm{compare}(a, b)$.

ULift.instMax_mathlib instance

[Max α] : Max (ULift.{v} α)

Full source

instance [Max α] : Max (ULift.{v} α) where max x y := up <| x.down ⊔ y.down

Maximum Operation on Lifted Types

Informal description

For any type $\alpha$ equipped with a maximum operation $\sqcup$, the lifted type $\mathrm{ULift}.\alpha$ also has a maximum operation, defined by lifting the operation from $\alpha$.

ULift.up_sup theorem

[Max α] (a b : α) : up (a ⊔ b) = up a ⊔ up b

Full source

@[simp] theorem up_sup [Max α] (a b : α) : up (a ⊔ b) = upup a ⊔ up b := rfl

Lifting Preserves Maximum: $\mathrm{up}(a \sqcup b) = \mathrm{up}(a) \sqcup \mathrm{up}(b)$

Informal description

For any type $\alpha$ equipped with a maximum operation $\sqcup$ and any elements $a, b \in \alpha$, the lift of the maximum of $a$ and $b$ is equal to the maximum of the lifts of $a$ and $b$ in $\mathrm{ULift}\,\alpha$. That is, $\mathrm{up}(a \sqcup b) = \mathrm{up}(a) \sqcup \mathrm{up}(b)$.

ULift.down_sup theorem

[Max α] (a b : ULift α) : down (a ⊔ b) = down a ⊔ down b

Full source

@[simp] theorem down_sup [Max α] (a b : ULift α) : down (a ⊔ b) = downdown a ⊔ down b := rfl

Down Projection Preserves Supremum in Lifted Types

Informal description

For any type $\alpha$ with a maximum operation $\sqcup$ and for any elements $a, b$ in the lifted type $\mathrm{ULift}\,\alpha$, the down projection of their supremum equals the supremum of their down projections, i.e., $\mathrm{down}(a \sqcup b) = \mathrm{down}(a) \sqcup \mathrm{down}(b)$.

ULift.instMin_mathlib instance

[Min α] : Min (ULift.{v} α)

Full source

instance [Min α] : Min (ULift.{v} α) where min x y := up <| x.down ⊓ y.down

Minimum Operation on Lifted Types

Informal description

For any type $\alpha$ equipped with a minimum operation $\sqcap$, the lifted type $\mathrm{ULift}\,\alpha$ also has a minimum operation, defined by lifting the operation from $\alpha$.

ULift.up_inf theorem

[Min α] (a b : α) : up (a ⊓ b) = up a ⊓ up b

Full source

@[simp] theorem up_inf [Min α] (a b : α) : up (a ⊓ b) = upup a ⊓ up b := rfl

Lifting Preserves Minimum: $\mathrm{up}(a \sqcap b) = \mathrm{up}(a) \sqcap \mathrm{up}(b)$

Informal description

For any type $\alpha$ equipped with a minimum operation $\sqcap$ and any elements $a, b \in \alpha$, the lift of the minimum of $a$ and $b$ is equal to the minimum of the lifts of $a$ and $b$ in $\mathrm{ULift}\,\alpha$. That is, $\mathrm{up}(a \sqcap b) = \mathrm{up}(a) \sqcap \mathrm{up}(b)$.

ULift.down_inf theorem

[Min α] (a b : ULift α) : down (a ⊓ b) = down a ⊓ down b

Full source

@[simp] theorem down_inf [Min α] (a b : ULift α) : down (a ⊓ b) = downdown a ⊓ down b := rfl

Projection of Infimum in Lifted Type Equals Infimum of Projections

Informal description

For any type $\alpha$ equipped with a minimum operation $\sqcap$ and any two elements $a, b$ in the lifted type $\mathrm{ULift}\,\alpha$, the projection of their infimum equals the infimum of their projections, i.e., $\mathrm{down}(a \sqcap b) = \mathrm{down}(a) \sqcap \mathrm{down}(b)$.

ULift.instSDiff_mathlib instance

[SDiff α] : SDiff (ULift.{v} α)

Full source

instance [SDiff α] : SDiff (ULift.{v} α) where sdiff x y := up <| x.down \ y.down

Lifted Set Difference Operation on ULift

Informal description

For any type $\alpha$ equipped with a set difference operation $\setminus$, the lifted type $\text{ULift} \alpha$ also has a set difference operation defined by lifting the operation from $\alpha$.

ULift.up_sdiff theorem

[SDiff α] (a b : α) : up (a \ b) = up a \ up b

Full source

@[simp] theorem up_sdiff [SDiff α] (a b : α) : up (a \ b) = upup a \ up b := rfl

Lifting Preserves Set Difference: $\text{up}(a \setminus b) = \text{up}(a) \setminus \text{up}(b)$

Informal description

For any type $\alpha$ equipped with a set difference operation $\setminus$, and for any elements $a, b \in \alpha$, the lifting of the set difference $a \setminus b$ to $\text{ULift} \alpha$ is equal to the set difference of the lifted elements $\text{up}(a) \setminus \text{up}(b)$.

ULift.down_sdiff theorem

[SDiff α] (a b : ULift α) : down (a \ b) = down a \ down b

Full source

@[simp] theorem down_sdiff [SDiff α] (a b : ULift α) : down (a \ b) = downdown a \ down b := rfl

Commutativity of Set Difference with Down Function in ULift

Informal description

For any type $\alpha$ equipped with a set difference operation $\setminus$ and for any elements $a, b$ in the lifted type $\text{ULift} \alpha$, the operation of taking the set difference commutes with the $\text{down}$ function, i.e., $\text{down}(a \setminus b) = \text{down}(a) \setminus \text{down}(b)$.

ULift.instHasCompl instance

[HasCompl α] : HasCompl (ULift.{v} α)

Full source

instance [HasCompl α] : HasCompl (ULift.{v} α) where compl x := up <| x.downᶜ

Lifted Complement Operation on ULift

Informal description

For any type $\alpha$ equipped with a complement operation $ᶜ$, the lifted type $\text{ULift} \alpha$ also has a complement operation, defined by lifting the complement operation from $\alpha$.

ULift.up_compl theorem

[HasCompl α] (a : α) : up (aᶜ) = (up a)ᶜ

Full source

@[simp] theorem up_compl [HasCompl α] (a : α) : up (aᶜ) = (up a)ᶜ := rfl

Complement Lifting Property in ULift

Informal description

For any type $\alpha$ equipped with a complement operation $ᶜ$ and any element $a \in \alpha$, the complement of the lifted element $\text{up}(a)$ in $\text{ULift} \alpha$ is equal to the lift of the complement of $a$ in $\alpha$, i.e., $\text{up}(aᶜ) = (\text{up}(a))ᶜ$.

ULift.down_compl theorem

[HasCompl α] (a : ULift α) : down aᶜ = (down a)ᶜ

Full source

@[simp] theorem down_compl [HasCompl α] (a : ULift α) : down aᶜ = (down a)ᶜ := rfl

Complement Projection Property in ULift

Informal description

For any type $\alpha$ equipped with a complement operation $ᶜ$ and any element $a$ in the lifted type $\text{ULift} \alpha$, the complement of $a$ in $\text{ULift} \alpha$ when projected back to $\alpha$ equals the complement of the projection of $a$ in $\alpha$, i.e., $\text{down}(aᶜ) = (\text{down}(a))ᶜ$.

ULift.instOrientedOrd_mathlib instance

[Ord α] [inst : OrientedOrd α] : OrientedOrd (ULift.{v} α)

Full source

instance [Ord α] [inst : OrientedOrd α] : OrientedOrd (ULift.{v} α) where
  symm _ _ := inst.symm ..

Oriented Order Structure on Lifted Types

Informal description

For any type $\alpha$ with an order structure and an orientation (given by `OrientedOrd α`), the lifted type `ULift.{v} α` inherits an oriented order structure where the orientation is preserved under the lifting operation.

ULift.instTransOrd_mathlib instance

[Ord α] [inst : TransOrd α] : TransOrd (ULift.{v} α)

Full source

instance [Ord α] [inst : TransOrd α] : TransOrd (ULift.{v} α) where
  le_trans := inst.le_trans

Transitive Order Structure on Lifted Types

Informal description

For any type $\alpha$ with an order structure and a transitive order relation (given by `TransOrd α`), the lifted type $\text{ULift} \alpha$ inherits a transitive order structure where the transitivity is preserved under the lifting operation.

ULift.instBEqOrd_mathlib instance

[BEq α] [Ord α] [inst : BEqOrd α] : BEqOrd (ULift.{v} α)

Full source

instance [BEq α] [Ord α] [inst : BEqOrd α] : BEqOrd (ULift.{v} α) where
  cmp_iff_beq := inst.cmp_iff_beq

Boolean Equality and Order Structure on Lifted Types

Informal description

For any type $\alpha$ equipped with both a boolean equality relation and an order structure that satisfy the `BEqOrd` typeclass, the lifted type $\text{ULift} \alpha$ also inherits a `BEqOrd` structure where both the equality and order relations are preserved under the lifting operation.

ULift.instLTOrd_mathlib instance

[LT α] [Ord α] [inst : LTOrd α] : LTOrd (ULift.{v} α)

Full source

instance [LT α] [Ord α] [inst : LTOrd α] : LTOrd (ULift.{v} α) where
  cmp_iff_lt := inst.cmp_iff_lt

Strict Order Structure Preservation in Lifted Types

Informal description

For any type $\alpha$ equipped with a strict order relation $<$ and an order structure (given by `Ord α`) that satisfies the `LTOrd` typeclass, the lifted type $\mathrm{ULift}\,\alpha$ inherits an `LTOrd` structure where the strict order relation is preserved under the lifting operation.

ULift.instLEOrd_mathlib instance

[LE α] [Ord α] [inst : LEOrd α] : LEOrd (ULift.{v} α)

Full source

instance [LE α] [Ord α] [inst : LEOrd α] : LEOrd (ULift.{v} α) where
  cmp_iff_le := inst.cmp_iff_le

Order Structure Preservation in Lifted Types

Informal description

For any type $\alpha$ equipped with a preorder (via the `LE` typeclass) and an order structure (via the `Ord` typeclass) that satisfies the `LEOrd` typeclass, the lifted type $\text{ULift} \alpha$ inherits an `LEOrd` structure where the order relations are preserved under the lifting operation.

ULift.instLawfulOrd_mathlib instance

[LE α] [LT α] [BEq α] [Ord α] [inst : LawfulOrd α] : LawfulOrd (ULift.{v} α)

Full source

instance [LE α] [LT α] [BEq α] [Ord α] [inst : LawfulOrd α] : LawfulOrd (ULift.{v} α) where
  cmp_iff_lt := inst.cmp_iff_lt
  cmp_iff_le := inst.cmp_iff_le

Preservation of Lawful Order Structure in Lifted Types

Informal description

For any type $\alpha$ equipped with a preorder (via `LE`), a strict order (via `LT`), a boolean equality relation (via `BEq`), and an order structure (via `Ord`) that together satisfy the `LawfulOrd` typeclass, the lifted type $\mathrm{ULift}\,\alpha$ inherits a `LawfulOrd` structure where all these relations are preserved under the lifting operation.

ULift.instPreorder instance

[Preorder α] : Preorder (ULift.{v} α)

Full source

instance [Preorder α] : Preorder (ULift.{v} α) :=
  Preorder.lift ULift.down

Preorder Structure on Lifted Types

Informal description

For any preorder $\alpha$, the lifted type $\text{ULift}.\{\nu\} \alpha$ inherits a preorder structure where the order relation is defined pointwise.

ULift.instPartialOrder instance

[PartialOrder α] : PartialOrder (ULift.{v} α)

Full source

instance [PartialOrder α] : PartialOrder (ULift.{v} α) :=
  PartialOrder.lift ULift.down ULift.down_injective

Partial Order Structure on Lifted Types

Informal description

For any partially ordered type $\alpha$, the lifted type $\text{ULift}.\{\nu\} \alpha$ inherits a partial order structure where the order relation is defined pointwise.