# Documentation

Mathlib.Data.Sum.Order

# Orders on a sum type #

This file defines the disjoint sum and the linear (aka lexicographic) sum of two orders and provides relation instances for Sum.LiftRel and Sum.Lex.

We declare the disjoint sum of orders as the default set of instances. The linear order goes on a type synonym.

## Main declarations #

• Sum.LE, Sum.LT: Disjoint sum of orders.
• Sum.Lex.LE, Sum.Lex.LT: Lexicographic/linear sum of orders.

## Notation #

• α ⊕ₗ β⊕ₗ β: The linear sum of α and β.

### Unbundled relation classes #

theorem Sum.LiftRel.refl {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsRefl α r] [inst : IsRefl β s] (x : α β) :
Sum.LiftRel r s x x
instance Sum.instIsReflSumLiftRel {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsRefl α r] [inst : IsRefl β s] :
IsRefl (α β) ()
Equations
instance Sum.instIsIrreflSumLiftRel {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsIrrefl α r] [inst : IsIrrefl β s] :
IsIrrefl (α β) ()
Equations
theorem Sum.LiftRel.trans {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsTrans α r] [inst : IsTrans β s] {a : α β} {b : α β} {c : α β} :
Sum.LiftRel r s a bSum.LiftRel r s b cSum.LiftRel r s a c
instance Sum.instIsTransSumLiftRel {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsTrans α r] [inst : IsTrans β s] :
IsTrans (α β) ()
Equations
instance Sum.instIsAntisymmSumLiftRel {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : ] [inst : ] :
IsAntisymm (α β) ()
Equations
instance Sum.instIsReflSumLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsRefl α r] [inst : IsRefl β s] :
IsRefl (α β) (Sum.Lex r s)
Equations
instance Sum.instIsIrreflSumLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsIrrefl α r] [inst : IsIrrefl β s] :
IsIrrefl (α β) (Sum.Lex r s)
Equations
instance Sum.instIsTransSumLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsTrans α r] [inst : IsTrans β s] :
IsTrans (α β) (Sum.Lex r s)
Equations
instance Sum.instIsAntisymmSumLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : ] [inst : ] :
IsAntisymm (α β) (Sum.Lex r s)
Equations
instance Sum.instIsTotalSumLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsTotal α r] [inst : IsTotal β s] :
IsTotal (α β) (Sum.Lex r s)
Equations
instance Sum.instIsTrichotomousSumLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : ] [inst : ] :
IsTrichotomous (α β) (Sum.Lex r s)
Equations
instance Sum.instIsWellOrderSumLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : ] [inst : ] :
IsWellOrder (α β) (Sum.Lex r s)
Equations

### Disjoint sum of two orders #

instance Sum.instLESum {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] :
LE (α β)
Equations
instance Sum.instLTSum {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] :
LT (α β)
Equations
• Sum.instLTSum = { lt := Sum.LiftRel (fun x x_1 => x < x_1) fun x x_1 => x < x_1 }
theorem Sum.le_def {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : α β} {b : α β} :
a b Sum.LiftRel (fun x x_1 => x x_1) (fun x x_1 => x x_1) a b
theorem Sum.lt_def {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : α β} {b : α β} :
a < b Sum.LiftRel (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) a b
@[simp]
theorem Sum.inl_le_inl_iff {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : α} {b : α} :
a b
@[simp]
theorem Sum.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : β} {b : β} :
a b
@[simp]
theorem Sum.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : α} {b : α} :
< a < b
@[simp]
theorem Sum.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : β} {b : β} :
< a < b
@[simp]
theorem Sum.not_inl_le_inr {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : α} {b : β} :
@[simp]
theorem Sum.not_inl_lt_inr {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : α} {b : β} :
¬ <
@[simp]
theorem Sum.not_inr_le_inl {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : α} {b : β} :
@[simp]
theorem Sum.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : α} {b : β} :
¬ <
instance Sum.instPreorderSum {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Preorder (α β)
Equations
• One or more equations did not get rendered due to their size.
theorem Sum.inl_mono {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Monotone Sum.inl
theorem Sum.inr_mono {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] :
Monotone Sum.inr
theorem Sum.inl_strictMono {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
StrictMono Sum.inl
theorem Sum.inr_strictMono {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] :
StrictMono Sum.inr
instance Sum.instPartialOrderSum {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Equations
instance Sum.noMinOrder {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : ] [inst : ] :
NoMinOrder (α β)
Equations
instance Sum.noMaxOrder {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : ] [inst : ] :
NoMaxOrder (α β)
Equations
@[simp]
theorem Sum.noMinOrder_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] :
NoMinOrder (α β)
@[simp]
theorem Sum.noMaxOrder_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] :
NoMaxOrder (α β)
instance Sum.denselyOrdered {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : ] [inst : ] :
Equations
@[simp]
theorem Sum.denselyOrdered_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] :
@[simp]
theorem Sum.swap_le_swap_iff {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : α β} {b : α β} :
a b
@[simp]
theorem Sum.swap_lt_swap_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : α β} {b : α β} :
a < b

### Linear sum of two orders #

The linear sum of two orders

Equations
@[match_pattern, inline]
abbrev Sum.inlₗ {α : Type u_1} {β : Type u_2} (x : α) :
Lex (α β)

Lexicographical sum.inl. Only used for pattern matching.

Equations
• = toLex ()
@[match_pattern, inline]
abbrev Sum.inrₗ {α : Type u_1} {β : Type u_2} (x : β) :
Lex (α β)

Lexicographical sum.inr. Only used for pattern matching.

Equations
• = toLex ()
instance Sum.Lex.LE {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] :
LE (Lex (α β))

The linear/lexicographical ≤≤ on a sum.

Equations
• Sum.Lex.LE = { le := Sum.Lex (fun x x_1 => x x_1) fun x x_1 => x x_1 }
instance Sum.Lex.LT {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] :
LT (Lex (α β))

The linear/lexicographical < on a sum.

Equations
• Sum.Lex.LT = { lt := Sum.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1 }
@[simp]
theorem Sum.Lex.toLex_le_toLex {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : α β} {b : α β} :
toLex a toLex b Sum.Lex (fun x x_1 => x x_1) (fun x x_1 => x x_1) a b
@[simp]
theorem Sum.Lex.toLex_lt_toLex {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : α β} {b : α β} :
toLex a < toLex b Sum.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) a b
theorem Sum.Lex.le_def {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : Lex (α β)} {b : Lex (α β)} :
a b Sum.Lex (fun x x_1 => x x_1) (fun x x_1 => x x_1) (ofLex a) (ofLex b)
theorem Sum.Lex.lt_def {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : Lex (α β)} {b : Lex (α β)} :
a < b Sum.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (ofLex a) (ofLex b)
theorem Sum.Lex.inl_le_inl_iff {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : α} {b : α} :
toLex () toLex () a b
theorem Sum.Lex.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : β} {b : β} :
toLex () toLex () a b
theorem Sum.Lex.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : α} {b : α} :
toLex () < toLex () a < b
theorem Sum.Lex.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : β} {b : β} :
toLex () < toLex () a < b
theorem Sum.Lex.inl_le_inr {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (a : α) (b : β) :
toLex () toLex ()
theorem Sum.Lex.inl_lt_inr {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] (a : α) (b : β) :
toLex () < toLex ()
theorem Sum.Lex.not_inr_le_inl {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : α} {b : β} :
¬toLex () toLex ()
theorem Sum.Lex.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : α} {b : β} :
¬toLex () < toLex ()
instance Sum.Lex.preorder {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Preorder (Lex (α β))
Equations
• One or more equations did not get rendered due to their size.
theorem Sum.Lex.toLex_mono {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Monotone toLex
theorem Sum.Lex.toLex_strictMono {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
StrictMono toLex
theorem Sum.Lex.inl_mono {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Monotone (toLex Sum.inl)
theorem Sum.Lex.inr_mono {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] :
Monotone (toLex Sum.inr)
theorem Sum.Lex.inl_strictMono {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
StrictMono (toLex Sum.inl)
theorem Sum.Lex.inr_strictMono {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] :
StrictMono (toLex Sum.inr)
instance Sum.Lex.partialOrder {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
PartialOrder (Lex (α β))
Equations
• One or more equations did not get rendered due to their size.
instance Sum.Lex.linearOrder {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
LinearOrder (Lex (α β))
Equations
• One or more equations did not get rendered due to their size.
instance Sum.Lex.orderBot {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : ] [inst : LE β] :
OrderBot (Lex (α β))

The lexicographical bottom of a sum is the bottom of the left component.

Equations
@[simp]
theorem Sum.Lex.inl_bot {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : ] [inst : LE β] :
toLex () =
instance Sum.Lex.orderTop {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] [inst : ] :
OrderTop (Lex (α β))

The lexicographical top of a sum is the top of the right component.

Equations
@[simp]
theorem Sum.Lex.inr_top {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] [inst : ] :
toLex () =
instance Sum.Lex.boundedOrder {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] [inst : ] [inst : ] :
BoundedOrder (Lex (α β))
Equations
• Sum.Lex.boundedOrder = let src := Sum.Lex.orderBot; let src_1 := Sum.Lex.orderTop; BoundedOrder.mk
instance Sum.Lex.noMinOrder {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : ] [inst : ] :
NoMinOrder (Lex (α β))
Equations
instance Sum.Lex.noMaxOrder {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : ] [inst : ] :
NoMaxOrder (Lex (α β))
Equations
instance Sum.Lex.noMinOrder_of_nonempty {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : ] [inst : ] :
NoMinOrder (Lex (α β))
Equations
instance Sum.Lex.noMaxOrder_of_nonempty {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : ] [inst : ] :
NoMaxOrder (Lex (α β))
Equations
instance Sum.Lex.denselyOrdered_of_noMaxOrder {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : ] [inst : ] [inst : ] :
Equations
instance Sum.Lex.denselyOrdered_of_noMinOrder {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : ] [inst : ] [inst : ] :
Equations

### Order isomorphisms #

@[simp]
theorem OrderIso.sumComm_apply (α : Type u_1) (β : Type u_2) [inst : LE α] [inst : LE β] :
∀ (a : α β), ().toEmbedding a =
def OrderIso.sumComm (α : Type u_1) (β : Type u_2) [inst : LE α] [inst : LE β] :
α β ≃o β α

Equiv.sumComm promoted to an order isomorphism.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem OrderIso.sumComm_symm (α : Type u_1) (β : Type u_2) [inst : LE α] [inst : LE β] :
def OrderIso.sumAssoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) [inst : LE α] [inst : LE β] [inst : LE γ] :
(α β) γ ≃o α β γ

Equiv.sumAssoc promoted to an order isomorphism.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem OrderIso.sumAssoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (a : α) :
().toEmbedding (Sum.inl ()) =
@[simp]
theorem OrderIso.sumAssoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (b : β) :
().toEmbedding (Sum.inl ()) = Sum.inr ()
@[simp]
theorem OrderIso.sumAssoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (c : γ) :
().toEmbedding () = Sum.inr ()
@[simp]
theorem OrderIso.sumAssoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (a : α) :
().toEmbedding () = Sum.inl ()
@[simp]
theorem OrderIso.sumAssoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (b : β) :
().toEmbedding (Sum.inr ()) = Sum.inl ()
@[simp]
theorem OrderIso.sumAssoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (c : γ) :
().toEmbedding (Sum.inr ()) =
def OrderIso.sumDualDistrib (α : Type u_1) (β : Type u_2) [inst : LE α] [inst : LE β] :

orderDual is distributive over ⊕⊕ up to an order isomorphism.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem OrderIso.sumDualDistrib_inl {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (a : α) :
().toEmbedding (OrderDual.toDual ()) = Sum.inl (OrderDual.toDual a)
@[simp]
theorem OrderIso.sumDualDistrib_inr {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (b : β) :
().toEmbedding (OrderDual.toDual ()) = Sum.inr (OrderDual.toDual b)
@[simp]
theorem OrderIso.sumDualDistrib_symm_inl {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (a : α) :
().toEmbedding (Sum.inl (OrderDual.toDual a)) = OrderDual.toDual ()
@[simp]
theorem OrderIso.sumDualDistrib_symm_inr {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (b : β) :
().toEmbedding (Sum.inr (OrderDual.toDual b)) = OrderDual.toDual ()
def OrderIso.sumLexAssoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) [inst : LE α] [inst : LE β] [inst : LE γ] :
Lex (Lex (α β) γ) ≃o Lex (α Lex (β γ))

Equiv.SumAssoc promoted to an order isomorphism.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem OrderIso.sumLexAssoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (a : α) :
().toEmbedding (toLex (Sum.inl (toLex ()))) = toLex ()
@[simp]
theorem OrderIso.sumLexAssoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (b : β) :
().toEmbedding (toLex (Sum.inl (toLex ()))) = toLex (Sum.inr (toLex ()))
@[simp]
theorem OrderIso.sumLexAssoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (c : γ) :
().toEmbedding (toLex ()) = toLex (Sum.inr (toLex ()))
@[simp]
theorem OrderIso.sumLexAssoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (a : α) :
().toEmbedding () = Sum.inl ()
@[simp]
theorem OrderIso.sumLexAssoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (b : β) :
().toEmbedding (Sum.inr ()) = Sum.inl ()
@[simp]
theorem OrderIso.sumLexAssoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (c : γ) :
().toEmbedding (Sum.inr ()) =
def OrderIso.sumLexDualAntidistrib (α : Type u_1) (β : Type u_2) [inst : LE α] [inst : LE β] :

OrderDual is antidistributive over ⊕ₗ⊕ₗ up to an order isomorphism.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem OrderIso.sumLexDualAntidistrib_inl {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (a : α) :
().toEmbedding (OrderDual.toDual ()) = Sum.inr (OrderDual.toDual a)
@[simp]
theorem OrderIso.sumLexDualAntidistrib_inr {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (b : β) :
().toEmbedding (OrderDual.toDual ()) = Sum.inl (OrderDual.toDual b)
@[simp]
theorem OrderIso.sumLexDualAntidistrib_symm_inl {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (b : β) :
().toEmbedding (Sum.inl (OrderDual.toDual b)) = OrderDual.toDual ()
@[simp]
theorem OrderIso.sumLexDualAntidistrib_symm_inr {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (a : α) :
().toEmbedding (Sum.inr (OrderDual.toDual a)) = OrderDual.toDual ()
def WithBot.orderIsoPUnitSumLex {α : Type u_1} [inst : LE α] :
≃o Lex ()

WithBot α is order-isomorphic to PUnit ⊕ₗ α⊕ₗ α, by sending ⊥⊥ to unit and ↑a↑a to a.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem WithBot.orderIsoPUnitSumLex_bot {α : Type u_1} [inst : LE α] :
(RelIso.toRelEmbedding WithBot.orderIsoPUnitSumLex).toEmbedding = toLex ()
@[simp]
theorem WithBot.orderIsoPUnitSumLex_toLex {α : Type u_1} [inst : LE α] (a : α) :
(RelIso.toRelEmbedding WithBot.orderIsoPUnitSumLex).toEmbedding a = toLex ()
@[simp]
theorem WithBot.orderIsoPUnitSumLex_symm_inl {α : Type u_2} [inst : LE α] (x : PUnit) :
(RelIso.toRelEmbedding (OrderIso.symm WithBot.orderIsoPUnitSumLex)).toEmbedding (toLex ()) =
@[simp]
theorem WithBot.orderIsoPUnitSumLex_symm_inr {α : Type u_1} [inst : LE α] (a : α) :
(RelIso.toRelEmbedding (OrderIso.symm WithBot.orderIsoPUnitSumLex)).toEmbedding (toLex ()) = a
def WithTop.orderIsoSumLexPUnit {α : Type u_1} [inst : LE α] :
≃o Lex ()

WithTop α is order-isomorphic to α ⊕ₗ PUnit⊕ₗ PUnit, by sending ⊤⊤ to unit and ↑a↑a to a.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem WithTop.orderIsoSumLexPUnit_top {α : Type u_1} [inst : LE α] :
(RelIso.toRelEmbedding WithTop.orderIsoSumLexPUnit).toEmbedding = toLex ()
@[simp]
theorem WithTop.orderIsoSumLexPUnit_toLex {α : Type u_1} [inst : LE α] (a : α) :
(RelIso.toRelEmbedding WithTop.orderIsoSumLexPUnit).toEmbedding a = toLex ()
@[simp]
theorem WithTop.orderIsoSumLexPUnit_symm_inr {α : Type u_2} [inst : LE α] (x : PUnit) :
(RelIso.toRelEmbedding (OrderIso.symm WithTop.orderIsoSumLexPUnit)).toEmbedding (toLex ()) =
@[simp]
theorem WithTop.orderIsoSumLexPUnit_symm_inl {α : Type u_1} [inst : LE α] (a : α) :
(RelIso.toRelEmbedding (OrderIso.symm WithTop.orderIsoSumLexPUnit)).toEmbedding (toLex ()) = a