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) [IsRefl α r] [IsRefl β s] (x : α ⊕ β) : LiftRel r s x x

instance Sum.instIsReflLiftRel {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsRefl α r] [IsRefl β s] : IsRefl (α ⊕ β) (LiftRel r s)

instance Sum.instIsIrreflLiftRel {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsIrrefl α r] [IsIrrefl β s] : IsIrrefl (α ⊕ β) (LiftRel r s)

theorem Sum.LiftRel.trans {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsTrans α r] [IsTrans β s] {a b c : α ⊕ β} : LiftRel r s a b → LiftRel r s b c → LiftRel r s a c

instance Sum.instIsTransLiftRel {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsTrans α r] [IsTrans β s] : IsTrans (α ⊕ β) (LiftRel r s)

instance Sum.instIsAntisymmLiftRel {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsAntisymm α r] [IsAntisymm β s] : IsAntisymm (α ⊕ β) (LiftRel r s)

instance Sum.instIsReflLex {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsRefl α r] [IsRefl β s] : IsRefl (α ⊕ β) (Lex r s)

instance Sum.instIsIrreflLex {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsIrrefl α r] [IsIrrefl β s] : IsIrrefl (α ⊕ β) (Lex r s)

instance Sum.instIsTransLex {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsTrans α r] [IsTrans β s] : IsTrans (α ⊕ β) (Lex r s)

instance Sum.instIsAntisymmLex {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsAntisymm α r] [IsAntisymm β s] : IsAntisymm (α ⊕ β) (Lex r s)

instance Sum.instIsTotalLex {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsTotal α r] [IsTotal β s] : IsTotal (α ⊕ β) (Lex r s)

instance Sum.instIsTrichotomousLex {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsTrichotomous α r] [IsTrichotomous β s] : IsTrichotomous (α ⊕ β) (Lex r s)

instance Sum.instIsWellOrderLex {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsWellOrder α r] [IsWellOrder β s] : IsWellOrder (α ⊕ β) (Lex r s)

Disjoint sum of two orders

instance Sum.instLESum {α : Type u_1} {β : Type u_2} [LE α] [LE β] : LE (α ⊕ β)

Equations

• Sum.instLESum = { le := Sum.LiftRel (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : β) => x1 ≤ x2 }

instance Sum.instLTSum {α : Type u_1} {β : Type u_2} [LT α] [LT β] : LT (α ⊕ β)

Equations

• Sum.instLTSum = { lt := Sum.LiftRel (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2 }

theorem Sum.le_def {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : α ⊕ β} : a ≤ b ↔ LiftRel (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) a b

theorem Sum.lt_def {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : α ⊕ β} : a < b ↔ LiftRel (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : β) => x1 < x2) a b

@[simp]

theorem Sum.inl_le_inl_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : α} : inl a ≤ inl b ↔ a ≤ b

@[simp]

theorem Sum.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : β} : inr a ≤ inr b ↔ a ≤ b

@[simp]

theorem Sum.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : α} : inl a < inl b ↔ a < b

@[simp]

theorem Sum.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : β} : inr a < inr b ↔ a < b

@[simp]

theorem Sum.not_inl_le_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : α} {b : β} : ¬inl b ≤ inr a

@[simp]

theorem Sum.not_inl_lt_inr {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : α} {b : β} : ¬inl b < inr a

@[simp]

theorem Sum.not_inr_le_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : α} {b : β} : ¬inr b ≤ inl a

@[simp]

theorem Sum.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : α} {b : β} : ¬inr b < inl a

instance Sum.instPreorderSum {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : Preorder (α ⊕ β)

Equations

• Sum.instPreorderSum = Preorder.mk ⋯ ⋯ ⋯

theorem Sum.inl_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : Monotone inl

theorem Sum.inr_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : Monotone inr

theorem Sum.inl_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : StrictMono inl

theorem Sum.inr_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : StrictMono inr

instance Sum.instPartialOrder {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] : PartialOrder (α ⊕ β)

Equations

• Sum.instPartialOrder = PartialOrder.mk ⋯

instance Sum.noMinOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMinOrder α] [NoMinOrder β] : NoMinOrder (α ⊕ β)

instance Sum.noMaxOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMaxOrder α] [NoMaxOrder β] : NoMaxOrder (α ⊕ β)

@[simp]

theorem Sum.noMinOrder_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] : NoMinOrder (α ⊕ β) ↔ NoMinOrder α ∧ NoMinOrder β

@[simp]

theorem Sum.noMaxOrder_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] : NoMaxOrder (α ⊕ β) ↔ NoMaxOrder α ∧ NoMaxOrder β

instance Sum.denselyOrdered {α : Type u_1} {β : Type u_2} [LT α] [LT β] [DenselyOrdered α] [DenselyOrdered β] : DenselyOrdered (α ⊕ β)

@[simp]

theorem Sum.denselyOrdered_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] : DenselyOrdered (α ⊕ β) ↔ DenselyOrdered α ∧ DenselyOrdered β

@[simp]

theorem Sum.swap_le_swap_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : α ⊕ β} : a.swap ≤ b.swap ↔ a ≤ b

@[simp]

theorem Sum.swap_lt_swap_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : α ⊕ β} : a.swap < b.swap ↔ a < b

Linear sum of two orders

def Sum.Lex.«term_⊕ₗ_» : Lean.TrailingParserDescr

The linear sum of two orders

Equations

• Sum.Lex.«term_⊕ₗ_» = Lean.ParserDescr.trailingNode `Sum.Lex.«term_⊕ₗ_» 30 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ₗ ") (Lean.ParserDescr.cat `term 29))

@[reducible, match_pattern, inline]

abbrev Sum.inlₗ {α : Type u_1} {β : Type u_2} (x : α) : _root_.Lex (α ⊕ β)

Lexicographical Sum.inl. Only used for pattern matching.

Equations

• Sum.inlₗ x = toLex (Sum.inl x)

@[reducible, match_pattern, inline]

abbrev Sum.inrₗ {α : Type u_1} {β : Type u_2} (x : β) : _root_.Lex (α ⊕ β)

Lexicographical Sum.inr. Only used for pattern matching.

Equations

• Sum.inrₗ x = toLex (Sum.inr x)

instance Sum.Lex.LE {α : Type u_1} {β : Type u_2} [LE α] [LE β] : LE (_root_.Lex (α ⊕ β))

The linear/lexicographical ≤ on a sum.

Equations

• Sum.Lex.LE = { le := Sum.Lex (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : β) => x1 ≤ x2 }

instance Sum.Lex.LT {α : Type u_1} {β : Type u_2} [LT α] [LT β] : LT (_root_.Lex (α ⊕ β))

The linear/lexicographical < on a sum.

Equations

• Sum.Lex.LT = { lt := Sum.Lex (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2 }

@[simp]

theorem Sum.Lex.toLex_le_toLex {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : α ⊕ β} : toLex a ≤ toLex b ↔ Lex (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) a b

@[simp]

theorem Sum.Lex.toLex_lt_toLex {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : α ⊕ β} : toLex a < toLex b ↔ Lex (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : β) => x1 < x2) a b

theorem Sum.Lex.le_def {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : _root_.Lex (α ⊕ β)} : a ≤ b ↔ Lex (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) (ofLex a) (ofLex b)

theorem Sum.Lex.lt_def {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : _root_.Lex (α ⊕ β)} : a < b ↔ Lex (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : β) => x1 < x2) (ofLex a) (ofLex b)

theorem Sum.Lex.inl_le_inl_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : α} : toLex (inl a) ≤ toLex (inl b) ↔ a ≤ b

theorem Sum.Lex.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : β} : toLex (inr a) ≤ toLex (inr b) ↔ a ≤ b

theorem Sum.Lex.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : α} : toLex (inl a) < toLex (inl b) ↔ a < b

theorem Sum.Lex.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : β} : toLex (inr a) < toLex (inr b) ↔ a < b

theorem Sum.Lex.inl_le_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a : α) (b : β) : toLex (inl a) ≤ toLex (inr b)

theorem Sum.Lex.inl_lt_inr {α : Type u_1} {β : Type u_2} [LT α] [LT β] (a : α) (b : β) : toLex (inl a) < toLex (inr b)

theorem Sum.Lex.not_inr_le_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : α} {b : β} : ¬toLex (inr b) ≤ toLex (inl a)

theorem Sum.Lex.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : α} {b : β} : ¬toLex (inr b) < toLex (inl a)

instance Sum.Lex.preorder {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : Preorder (_root_.Lex (α ⊕ β))

Equations

• Sum.Lex.preorder = Preorder.mk ⋯ ⋯ ⋯

theorem Sum.Lex.toLex_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : Monotone ⇑toLex

theorem Sum.Lex.toLex_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : StrictMono ⇑toLex

theorem Sum.Lex.inl_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : Monotone (⇑toLex ∘ inl)

theorem Sum.Lex.inr_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : Monotone (⇑toLex ∘ inr)

theorem Sum.Lex.inl_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : StrictMono (⇑toLex ∘ inl)

theorem Sum.Lex.inr_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : StrictMono (⇑toLex ∘ inr)

instance Sum.Lex.partialOrder {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] : PartialOrder (_root_.Lex (α ⊕ β))

Equations

• Sum.Lex.partialOrder = PartialOrder.mk ⋯

instance Sum.Lex.linearOrder {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] : LinearOrder (_root_.Lex (α ⊕ β))

Equations

• Sum.Lex.linearOrder = LinearOrder.mk ⋯ Sum.instDecidableRelSumLex instDecidableEqSum decidableLTOfDecidableLE ⋯ ⋯ ⋯

instance Sum.Lex.orderBot {α : Type u_1} {β : Type u_2} [LE α] [OrderBot α] [LE β] : OrderBot (_root_.Lex (α ⊕ β))

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

Equations

• Sum.Lex.orderBot = OrderBot.mk ⋯

@[simp]

theorem Sum.Lex.inl_bot {α : Type u_1} {β : Type u_2} [LE α] [OrderBot α] [LE β] : toLex (inl ⊥) = ⊥

instance Sum.Lex.orderTop {α : Type u_1} {β : Type u_2} [LE α] [LE β] [OrderTop β] : OrderTop (_root_.Lex (α ⊕ β))

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

Equations

• Sum.Lex.orderTop = OrderTop.mk ⋯

@[simp]

theorem Sum.Lex.inr_top {α : Type u_1} {β : Type u_2} [LE α] [LE β] [OrderTop β] : toLex (inr ⊤) = ⊤

instance Sum.Lex.boundedOrder {α : Type u_1} {β : Type u_2} [LE α] [LE β] [OrderBot α] [OrderTop β] : BoundedOrder (_root_.Lex (α ⊕ β))

Equations

• Sum.Lex.boundedOrder = BoundedOrder.mk

instance Sum.Lex.noMinOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMinOrder α] [NoMinOrder β] : NoMinOrder (_root_.Lex (α ⊕ β))

instance Sum.Lex.noMaxOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMaxOrder α] [NoMaxOrder β] : NoMaxOrder (_root_.Lex (α ⊕ β))

instance Sum.Lex.noMinOrder_of_nonempty {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMinOrder α] [Nonempty α] : NoMinOrder (_root_.Lex (α ⊕ β))

instance Sum.Lex.noMaxOrder_of_nonempty {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMaxOrder β] [Nonempty β] : NoMaxOrder (_root_.Lex (α ⊕ β))

instance Sum.Lex.denselyOrdered_of_noMaxOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [DenselyOrdered α] [DenselyOrdered β] [NoMaxOrder α] : DenselyOrdered (_root_.Lex (α ⊕ β))

instance Sum.Lex.denselyOrdered_of_noMinOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [DenselyOrdered α] [DenselyOrdered β] [NoMinOrder β] : DenselyOrdered (_root_.Lex (α ⊕ β))

Order isomorphisms

def OrderIso.sumComm (α : Type u_4) (β : Type u_5) [LE α] [LE β] : α ⊕ β ≃o β ⊕ α

Equiv.sumComm promoted to an order isomorphism.

Equations

• OrderIso.sumComm α β = { toEquiv := Equiv.sumComm α β, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.sumComm_apply (α : Type u_4) (β : Type u_5) [LE α] [LE β] (a✝ : α ⊕ β) : (sumComm α β) a✝ = a✝.swap

@[simp]

theorem OrderIso.sumComm_symm (α : Type u_4) (β : Type u_5) [LE α] [LE β] : (sumComm α β).symm = sumComm β α

def OrderIso.sumAssoc (α : Type u_4) (β : Type u_5) (γ : Type u_6) [LE α] [LE β] [LE γ] : (α ⊕ β) ⊕ γ ≃o α ⊕ β ⊕ γ

Equiv.sumAssoc promoted to an order isomorphism.

Equations

• OrderIso.sumAssoc α β γ = { toEquiv := Equiv.sumAssoc α β γ, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.sumAssoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (a : α) : (sumAssoc α β γ) (Sum.inl (Sum.inl a)) = Sum.inl a

@[simp]

theorem OrderIso.sumAssoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (b : β) : (sumAssoc α β γ) (Sum.inl (Sum.inr b)) = Sum.inr (Sum.inl b)

@[simp]

theorem OrderIso.sumAssoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (c : γ) : (sumAssoc α β γ) (Sum.inr c) = Sum.inr (Sum.inr c)

@[simp]

theorem OrderIso.sumAssoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (a : α) : (sumAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)

@[simp]

theorem OrderIso.sumAssoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (b : β) : (sumAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)

@[simp]

theorem OrderIso.sumAssoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (c : γ) : (sumAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c

def OrderIso.sumDualDistrib (α : Type u_4) (β : Type u_5) [LE α] [LE β] : (α ⊕ β)ᵒᵈ ≃o αᵒᵈ ⊕ βᵒᵈ

orderDual is distributive over ⊕ up to an order isomorphism.

Equations

• OrderIso.sumDualDistrib α β = { toEquiv := Equiv.refl (α ⊕ β)ᵒᵈ, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.sumDualDistrib_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a : α) : (sumDualDistrib α β) (OrderDual.toDual (Sum.inl a)) = Sum.inl (OrderDual.toDual a)

@[simp]

theorem OrderIso.sumDualDistrib_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (b : β) : (sumDualDistrib α β) (OrderDual.toDual (Sum.inr b)) = Sum.inr (OrderDual.toDual b)

@[simp]

theorem OrderIso.sumDualDistrib_symm_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a : α) : (sumDualDistrib α β).symm (Sum.inl (OrderDual.toDual a)) = OrderDual.toDual (Sum.inl a)

@[simp]

theorem OrderIso.sumDualDistrib_symm_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (b : β) : (sumDualDistrib α β).symm (Sum.inr (OrderDual.toDual b)) = OrderDual.toDual (Sum.inr b)

def OrderIso.sumLexAssoc (α : Type u_4) (β : Type u_5) (γ : Type u_6) [LE α] [LE β] [LE γ] : Lex (Lex (α ⊕ β) ⊕ γ) ≃o Lex (α ⊕ Lex (β ⊕ γ))

Equiv.SumAssoc promoted to an order isomorphism.

Equations

• OrderIso.sumLexAssoc α β γ = { toEquiv := Equiv.sumAssoc α β γ, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.sumLexAssoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (a : α) : (sumLexAssoc α β γ) (toLex (Sum.inl (toLex (Sum.inl a)))) = toLex (Sum.inl a)

@[simp]

theorem OrderIso.sumLexAssoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (b : β) : (sumLexAssoc α β γ) (toLex (Sum.inl (toLex (Sum.inr b)))) = toLex (Sum.inr (toLex (Sum.inl b)))

@[simp]

theorem OrderIso.sumLexAssoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (c : γ) : (sumLexAssoc α β γ) (toLex (Sum.inr c)) = toLex (Sum.inr (toLex (Sum.inr c)))

@[simp]

theorem OrderIso.sumLexAssoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (a : α) : (sumLexAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)

@[simp]

theorem OrderIso.sumLexAssoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (b : β) : (sumLexAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)

@[simp]

theorem OrderIso.sumLexAssoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (c : γ) : (sumLexAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c

def OrderIso.sumLexDualAntidistrib (α : Type u_4) (β : Type u_5) [LE α] [LE β] : (Lex (α ⊕ β))ᵒᵈ ≃o Lex (βᵒᵈ ⊕ αᵒᵈ)

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

Equations

• OrderIso.sumLexDualAntidistrib α β = { toEquiv := Equiv.sumComm α β, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.sumLexDualAntidistrib_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a : α) : (sumLexDualAntidistrib α β) (OrderDual.toDual (Sum.inl a)) = Sum.inr (OrderDual.toDual a)

@[simp]

theorem OrderIso.sumLexDualAntidistrib_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (b : β) : (sumLexDualAntidistrib α β) (OrderDual.toDual (Sum.inr b)) = Sum.inl (OrderDual.toDual b)

@[simp]

theorem OrderIso.sumLexDualAntidistrib_symm_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] (b : β) : (sumLexDualAntidistrib α β).symm (Sum.inl (OrderDual.toDual b)) = OrderDual.toDual (Sum.inr b)

@[simp]

theorem OrderIso.sumLexDualAntidistrib_symm_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a : α) : (sumLexDualAntidistrib α β).symm (Sum.inr (OrderDual.toDual a)) = OrderDual.toDual (Sum.inl a)

def WithBot.orderIsoPUnitSumLex {α : Type u_1} [LE α] : WithBot α ≃o Lex (PUnit.{u_4 + 1} ⊕ α)

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

Equations

• WithBot.orderIsoPUnitSumLex = { toEquiv := (Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit.{?u.21 + 1}).trans toLex), map_rel_iff' := ⋯ }

@[simp]

theorem WithBot.orderIsoPUnitSumLex_bot {α : Type u_1} [LE α] : orderIsoPUnitSumLex ⊥ = toLex (Sum.inl PUnit.unit)

@[simp]

theorem WithBot.orderIsoPUnitSumLex_toLex {α : Type u_1} [LE α] (a : α) : orderIsoPUnitSumLex ↑a = toLex (Sum.inr a)

@[simp]

theorem WithBot.orderIsoPUnitSumLex_symm_inl {α : Type u_1} [LE α] (x : PUnit.{u_4 + 1}) : orderIsoPUnitSumLex.symm (toLex (Sum.inl x)) = ⊥

@[simp]

theorem WithBot.orderIsoPUnitSumLex_symm_inr {α : Type u_1} [LE α] (a : α) : orderIsoPUnitSumLex.symm (toLex (Sum.inr a)) = ↑a

def WithTop.orderIsoSumLexPUnit {α : Type u_1} [LE α] : WithTop α ≃o Lex (α ⊕ PUnit.{u_4 + 1})

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

Equations

• WithTop.orderIsoSumLexPUnit = { toEquiv := (Equiv.optionEquivSumPUnit α).trans toLex, map_rel_iff' := ⋯ }

@[simp]

theorem WithTop.orderIsoSumLexPUnit_top {α : Type u_1} [LE α] : orderIsoSumLexPUnit ⊤ = toLex (Sum.inr PUnit.unit)

@[simp]

theorem WithTop.orderIsoSumLexPUnit_toLex {α : Type u_1} [LE α] (a : α) : orderIsoSumLexPUnit ↑a = toLex (Sum.inl a)

@[simp]

theorem WithTop.orderIsoSumLexPUnit_symm_inr {α : Type u_1} [LE α] (x : PUnit.{u_4 + 1}) : orderIsoSumLexPUnit.symm (toLex (Sum.inr x)) = ⊤

@[simp]

theorem WithTop.orderIsoSumLexPUnit_symm_inl {α : Type u_1} [LE α] (a : α) : orderIsoSumLexPUnit.symm (toLex (Sum.inl a)) = ↑a