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 #

source

ink

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

source

ink

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

IsRefl (α ⊕ β) (Sum.LiftRel r s)

Equations

@Sum.instIsReflSumLiftRel = @Sum.instIsReflSumLiftRel.proof_1

source

ink

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

IsIrrefl (α ⊕ β) (Sum.LiftRel r s)

Equations

@Sum.instIsIrreflSumLiftRel = @Sum.instIsIrreflSumLiftRel.proof_1

source

ink

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 b → Sum.LiftRel r s b c → Sum.LiftRel r s a c

source

ink

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

IsTrans (α ⊕ β) (Sum.LiftRel r s)

Equations

@Sum.instIsTransSumLiftRel = @Sum.instIsTransSumLiftRel.proof_1

source

ink

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

IsAntisymm (α ⊕ β) (Sum.LiftRel r s)

Equations

@Sum.instIsAntisymmSumLiftRel = @Sum.instIsAntisymmSumLiftRel.proof_1

source

ink

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

@Sum.instIsReflSumLex = @Sum.instIsReflSumLex.proof_1

source

ink

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

@Sum.instIsIrreflSumLex = @Sum.instIsIrreflSumLex.proof_1

source

ink

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

@Sum.instIsTransSumLex = @Sum.instIsTransSumLex.proof_1

source

ink

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

IsAntisymm (α ⊕ β) (Sum.Lex r s)

Equations

@Sum.instIsAntisymmSumLex = @Sum.instIsAntisymmSumLex.proof_1

source

ink

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

@Sum.instIsTotalSumLex = @Sum.instIsTotalSumLex.proof_1

source

ink

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

IsTrichotomous (α ⊕ β) (Sum.Lex r s)

Equations

@Sum.instIsTrichotomousSumLex = @Sum.instIsTrichotomousSumLex.proof_1

source

ink

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

IsWellOrder (α ⊕ β) (Sum.Lex r s)

Equations

@Sum.instIsWellOrderSumLex = @Sum.instIsWellOrderSumLex.proof_1

Disjoint sum of two orders #

source

ink

instance Sum.instLESum {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] :

LE (α ⊕ β)

Equations

Sum.instLESum = { le := Sum.LiftRel (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 }

source

ink

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 }

source

ink

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

source

ink

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

source

ink

@[simp]

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

Sum.inl a ≤ Sum.inl b ↔ a ≤ b

source

ink

@[simp]

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

Sum.inr a ≤ Sum.inr b ↔ a ≤ b

source

ink

@[simp]

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

Sum.inl a < Sum.inl b ↔ a < b

source

ink

@[simp]

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

Sum.inr a < Sum.inr b ↔ a < b

source

ink

@[simp]

theorem Sum.not_inl_le_inr {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : α} {b : β} :

¬Sum.inl b ≤ Sum.inr a

source

ink

@[simp]

theorem Sum.not_inl_lt_inr {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : α} {b : β} :

¬Sum.inl b < Sum.inr a

source

ink

@[simp]

theorem Sum.not_inr_le_inl {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : α} {b : β} :

¬Sum.inr b ≤ Sum.inl a

source

ink

@[simp]

theorem Sum.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : α} {b : β} :

¬Sum.inr b < Sum.inl a

source

ink

instance Sum.instPreorderSum {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] :

Preorder (α ⊕ β)

Equations

One or more equations did not get rendered due to their size.

source

ink

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

Monotone Sum.inl

source

ink

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

Monotone Sum.inr

source

ink

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

StrictMono Sum.inl

source

ink

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

StrictMono Sum.inr

source

ink

instance Sum.instPartialOrderSum {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] :

PartialOrder (α ⊕ β)

Equations

Sum.instPartialOrderSum = let src := Sum.instPreorderSum; PartialOrder.mk (_ : ∀ (x x_1 : α ⊕ β), Sum.LiftRel (fun x x_2 => x ≤ x_2) (fun x x_2 => x ≤ x_2) x x_1 → x_1 ≤ x → x = x_1)

source

ink

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

NoMinOrder (α ⊕ β)

Equations

@Sum.noMinOrder = @Sum.noMinOrder.proof_1

source

ink

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

NoMaxOrder (α ⊕ β)

Equations

@Sum.noMaxOrder = @Sum.noMaxOrder.proof_1

source

ink

@[simp]

theorem Sum.noMinOrder_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] :

NoMinOrder (α ⊕ β) ↔ NoMinOrder α ∧ NoMinOrder β

source

ink

@[simp]

theorem Sum.noMaxOrder_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] :

NoMaxOrder (α ⊕ β) ↔ NoMaxOrder α ∧ NoMaxOrder β

source

ink

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

DenselyOrdered (α ⊕ β)

Equations

@Sum.denselyOrdered = @Sum.denselyOrdered.proof_1

source

ink

@[simp]

theorem Sum.denselyOrdered_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] :

DenselyOrdered (α ⊕ β) ↔ DenselyOrdered α ∧ DenselyOrdered β

source

ink

@[simp]

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

Sum.swap a ≤ Sum.swap b ↔ a ≤ b

source

ink

@[simp]

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

Sum.swap a < Sum.swap b ↔ a < b

Linear sum of two orders #

source

ink

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))

source

ink

@[match_pattern, inline]

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

Lex (α ⊕ β)

Lexicographical sum.inl. Only used for pattern matching.

Equations

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

source

ink

@[match_pattern, inline]

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

Lex (α ⊕ β)

Lexicographical sum.inr. Only used for pattern matching.

Equations

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

source

ink

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 }

source

ink

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 }

source

ink

@[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

source

ink

@[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

source

ink

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)

source

ink

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)

source

ink

theorem Sum.Lex.inl_le_inl_iff {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : α} {b : α} :

↑toLex (Sum.inl a) ≤ ↑toLex (Sum.inl b) ↔ a ≤ b

source

ink

theorem Sum.Lex.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : β} {b : β} :

↑toLex (Sum.inr a) ≤ ↑toLex (Sum.inr b) ↔ a ≤ b

source

ink

theorem Sum.Lex.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : α} {b : α} :

↑toLex (Sum.inl a) < ↑toLex (Sum.inl b) ↔ a < b

source

ink

theorem Sum.Lex.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : β} {b : β} :

↑toLex (Sum.inr a) < ↑toLex (Sum.inr b) ↔ a < b

source

ink

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

↑toLex (Sum.inl a) ≤ ↑toLex (Sum.inr b)

source

ink

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

↑toLex (Sum.inl a) < ↑toLex (Sum.inr b)

source

ink

theorem Sum.Lex.not_inr_le_inl {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] {a : α} {b : β} :

¬↑toLex (Sum.inr b) ≤ ↑toLex (Sum.inl a)

source

ink

theorem Sum.Lex.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] {a : α} {b : β} :

¬↑toLex (Sum.inr b) < ↑toLex (Sum.inl a)

source

ink

instance Sum.Lex.preorder {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] :

Preorder (Lex (α ⊕ β))

Equations

One or more equations did not get rendered due to their size.

source

ink

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

Monotone ↑toLex

source

ink

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

StrictMono ↑toLex

source

ink

theorem Sum.Lex.inl_mono {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] :

Monotone (↑toLex ∘ Sum.inl)

source

ink

theorem Sum.Lex.inr_mono {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : Preorder β] :

Monotone (↑toLex ∘ Sum.inr)

source

ink

theorem Sum.Lex.inl_strictMono {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] :

StrictMono (↑toLex ∘ Sum.inl)

source

ink

theorem Sum.Lex.inr_strictMono {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : Preorder β] :

StrictMono (↑toLex ∘ Sum.inr)

source

ink

instance Sum.Lex.partialOrder {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] :

PartialOrder (Lex (α ⊕ β))

Equations

One or more equations did not get rendered due to their size.

source

ink

instance Sum.Lex.linearOrder {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : LinearOrder β] :

LinearOrder (Lex (α ⊕ β))

Equations

One or more equations did not get rendered due to their size.

source

ink

instance Sum.Lex.orderBot {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : LE β] :

OrderBot (Lex (α ⊕ β))

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

Equations

Sum.Lex.orderBot = OrderBot.mk (_ : ∀ (a : Lex (α ⊕ β)), ⊥ ≤ a)

source

ink

@[simp]

theorem Sum.Lex.inl_bot {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : LE β] :

↑toLex (Sum.inl ⊥) = ⊥

source

ink

instance Sum.Lex.orderTop {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] [inst : OrderTop β] :

OrderTop (Lex (α ⊕ β))

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

Equations

Sum.Lex.orderTop = OrderTop.mk (_ : ∀ (a : Lex (α ⊕ β)), a ≤ ⊤)

source

ink

@[simp]

theorem Sum.Lex.inr_top {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] [inst : OrderTop β] :

↑toLex (Sum.inr ⊤) = ⊤

source

ink

instance Sum.Lex.boundedOrder {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] [inst : OrderBot α] [inst : OrderTop β] :

BoundedOrder (Lex (α ⊕ β))

Equations

Sum.Lex.boundedOrder = let src := Sum.Lex.orderBot; let src_1 := Sum.Lex.orderTop; BoundedOrder.mk

source

ink

instance Sum.Lex.noMinOrder {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : NoMinOrder α] [inst : NoMinOrder β] :

NoMinOrder (Lex (α ⊕ β))

Equations

@Sum.Lex.noMinOrder = @Sum.Lex.noMinOrder.proof_1

source

ink

instance Sum.Lex.noMaxOrder {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : NoMaxOrder α] [inst : NoMaxOrder β] :

NoMaxOrder (Lex (α ⊕ β))

Equations

@Sum.Lex.noMaxOrder = @Sum.Lex.noMaxOrder.proof_1

source

ink

instance Sum.Lex.noMinOrder_of_nonempty {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : NoMinOrder α] [inst : Nonempty α] :

NoMinOrder (Lex (α ⊕ β))

Equations

@Sum.Lex.noMinOrder_of_nonempty = @Sum.Lex.noMinOrder_of_nonempty.proof_1

source

ink

instance Sum.Lex.noMaxOrder_of_nonempty {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : NoMaxOrder β] [inst : Nonempty β] :

NoMaxOrder (Lex (α ⊕ β))

Equations

@Sum.Lex.noMaxOrder_of_nonempty = @Sum.Lex.noMaxOrder_of_nonempty.proof_1

source

ink

instance Sum.Lex.denselyOrdered_of_noMaxOrder {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : DenselyOrdered α] [inst : DenselyOrdered β] [inst : NoMaxOrder α] :

DenselyOrdered (Lex (α ⊕ β))

Equations

@Sum.Lex.denselyOrdered_of_noMaxOrder = @Sum.Lex.denselyOrdered_of_noMaxOrder.proof_1

source

ink

instance Sum.Lex.denselyOrdered_of_noMinOrder {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] [inst : DenselyOrdered α] [inst : DenselyOrdered β] [inst : NoMinOrder β] :

DenselyOrdered (Lex (α ⊕ β))

Equations

@Sum.Lex.denselyOrdered_of_noMinOrder = @Sum.Lex.denselyOrdered_of_noMinOrder.proof_1

Order isomorphisms #

source

ink

@[simp]

theorem OrderIso.sumComm_apply (α : Type u_1) (β : Type u_2) [inst : LE α] [inst : LE β] :

∀ (a : α ⊕ β), ↑(RelIso.toRelEmbedding (OrderIso.sumComm α β)).toEmbedding a = Sum.swap a

source

ink

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.

source

ink

@[simp]

theorem OrderIso.sumComm_symm (α : Type u_1) (β : Type u_2) [inst : LE α] [inst : LE β] :

OrderIso.symm (OrderIso.sumComm α β) = OrderIso.sumComm β α

source

ink

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.

source

ink

@[simp]

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

↑(RelIso.toRelEmbedding (OrderIso.sumAssoc α β γ)).toEmbedding (Sum.inl (Sum.inl a)) = Sum.inl a

source

ink

@[simp]

theorem OrderIso.sumAssoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (b : β) :

↑(RelIso.toRelEmbedding (OrderIso.sumAssoc α β γ)).toEmbedding (Sum.inl (Sum.inr b)) = Sum.inr (Sum.inl b)

source

ink

@[simp]

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

↑(RelIso.toRelEmbedding (OrderIso.sumAssoc α β γ)).toEmbedding (Sum.inr c) = Sum.inr (Sum.inr c)

source

ink

@[simp]

theorem OrderIso.sumAssoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (a : α) :

↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumAssoc α β γ))).toEmbedding (Sum.inl a) = Sum.inl (Sum.inl a)

source

ink

@[simp]

theorem OrderIso.sumAssoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (b : β) :

↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumAssoc α β γ))).toEmbedding (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)

source

ink

@[simp]

theorem OrderIso.sumAssoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (c : γ) :

↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumAssoc α β γ))).toEmbedding (Sum.inr (Sum.inr c)) = Sum.inr c

source

ink

def OrderIso.sumDualDistrib (α : Type u_1) (β : Type u_2) [inst : LE α] [inst : LE β] :

(α ⊕ β)ᵒᵈ ≃o αᵒᵈ ⊕ βᵒᵈ

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

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem OrderIso.sumDualDistrib_inl {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (a : α) :

↑(RelIso.toRelEmbedding (OrderIso.sumDualDistrib α β)).toEmbedding (↑OrderDual.toDual (Sum.inl a)) = Sum.inl (↑OrderDual.toDual a)

source

ink

@[simp]

theorem OrderIso.sumDualDistrib_inr {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (b : β) :

↑(RelIso.toRelEmbedding (OrderIso.sumDualDistrib α β)).toEmbedding (↑OrderDual.toDual (Sum.inr b)) = Sum.inr (↑OrderDual.toDual b)

source

ink

@[simp]

theorem OrderIso.sumDualDistrib_symm_inl {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (a : α) :

↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumDualDistrib α β))).toEmbedding (Sum.inl (↑OrderDual.toDual a)) = ↑OrderDual.toDual (Sum.inl a)

source

ink

@[simp]

theorem OrderIso.sumDualDistrib_symm_inr {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (b : β) :

↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumDualDistrib α β))).toEmbedding (Sum.inr (↑OrderDual.toDual b)) = ↑OrderDual.toDual (Sum.inr b)

source

ink

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.

source

ink

@[simp]

theorem OrderIso.sumLexAssoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (a : α) :

↑(RelIso.toRelEmbedding (OrderIso.sumLexAssoc α β γ)).toEmbedding (↑toLex (Sum.inl (↑toLex (Sum.inl a)))) = ↑toLex (Sum.inl a)

source

ink

@[simp]

theorem OrderIso.sumLexAssoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (b : β) :

↑(RelIso.toRelEmbedding (OrderIso.sumLexAssoc α β γ)).toEmbedding (↑toLex (Sum.inl (↑toLex (Sum.inr b)))) = ↑toLex (Sum.inr (↑toLex (Sum.inl b)))

source

ink

@[simp]

theorem OrderIso.sumLexAssoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (c : γ) :

↑(RelIso.toRelEmbedding (OrderIso.sumLexAssoc α β γ)).toEmbedding (↑toLex (Sum.inr c)) = ↑toLex (Sum.inr (↑toLex (Sum.inr c)))

source

ink

@[simp]

theorem OrderIso.sumLexAssoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (a : α) :

↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumLexAssoc α β γ))).toEmbedding (Sum.inl a) = Sum.inl (Sum.inl a)

source

ink

@[simp]

theorem OrderIso.sumLexAssoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (b : β) :

↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumLexAssoc α β γ))).toEmbedding (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)

source

ink

@[simp]

theorem OrderIso.sumLexAssoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst : LE β] [inst : LE γ] (c : γ) :

↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumLexAssoc α β γ))).toEmbedding (Sum.inr (Sum.inr c)) = Sum.inr c

source

ink

def OrderIso.sumLexDualAntidistrib (α : Type u_1) (β : Type u_2) [inst : LE α] [inst : LE β] :

(Lex (α ⊕ β))ᵒᵈ ≃o Lex (βᵒᵈ ⊕ αᵒᵈ)

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

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem OrderIso.sumLexDualAntidistrib_inl {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (a : α) :

↑(RelIso.toRelEmbedding (OrderIso.sumLexDualAntidistrib α β)).toEmbedding (↑OrderDual.toDual (Sum.inl a)) = Sum.inr (↑OrderDual.toDual a)

source

ink

@[simp]

theorem OrderIso.sumLexDualAntidistrib_inr {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (b : β) :

↑(RelIso.toRelEmbedding (OrderIso.sumLexDualAntidistrib α β)).toEmbedding (↑OrderDual.toDual (Sum.inr b)) = Sum.inl (↑OrderDual.toDual b)

source

ink

@[simp]

theorem OrderIso.sumLexDualAntidistrib_symm_inl {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (b : β) :

↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumLexDualAntidistrib α β))).toEmbedding (Sum.inl (↑OrderDual.toDual b)) = ↑OrderDual.toDual (Sum.inr b)

source

ink

@[simp]

theorem OrderIso.sumLexDualAntidistrib_symm_inr {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] (a : α) :

↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.sumLexDualAntidistrib α β))).toEmbedding (Sum.inr (↑OrderDual.toDual a)) = ↑OrderDual.toDual (Sum.inl a)

source

ink

def WithBot.orderIsoPUnitSumLex {α : Type u_1} [inst : LE α] :

WithBot α ≃o Lex (PUnit ⊕ α)

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.

source

ink

@[simp]

theorem WithBot.orderIsoPUnitSumLex_bot {α : Type u_1} [inst : LE α] :

↑(RelIso.toRelEmbedding WithBot.orderIsoPUnitSumLex).toEmbedding ⊥ = ↑toLex (Sum.inl PUnit.unit)

source

ink

@[simp]

theorem WithBot.orderIsoPUnitSumLex_toLex {α : Type u_1} [inst : LE α] (a : α) :

↑(RelIso.toRelEmbedding WithBot.orderIsoPUnitSumLex).toEmbedding ↑a = ↑toLex (Sum.inr a)

source

ink

@[simp]

theorem WithBot.orderIsoPUnitSumLex_symm_inl {α : Type u_2} [inst : LE α] (x : PUnit) :

↑(RelIso.toRelEmbedding (OrderIso.symm WithBot.orderIsoPUnitSumLex)).toEmbedding (↑toLex (Sum.inl x)) = ⊥

source

ink

@[simp]

theorem WithBot.orderIsoPUnitSumLex_symm_inr {α : Type u_1} [inst : LE α] (a : α) :

↑(RelIso.toRelEmbedding (OrderIso.symm WithBot.orderIsoPUnitSumLex)).toEmbedding (↑toLex (Sum.inr a)) = ↑a

source

ink

def WithTop.orderIsoSumLexPUnit {α : Type u_1} [inst : LE α] :

WithTop α ≃o Lex (α ⊕ PUnit)

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.

source

ink

@[simp]

theorem WithTop.orderIsoSumLexPUnit_top {α : Type u_1} [inst : LE α] :

↑(RelIso.toRelEmbedding WithTop.orderIsoSumLexPUnit).toEmbedding ⊤ = ↑toLex (Sum.inr PUnit.unit)

source

ink

@[simp]

theorem WithTop.orderIsoSumLexPUnit_toLex {α : Type u_1} [inst : LE α] (a : α) :

↑(RelIso.toRelEmbedding WithTop.orderIsoSumLexPUnit).toEmbedding ↑a = ↑toLex (Sum.inl a)

source

ink

@[simp]

theorem WithTop.orderIsoSumLexPUnit_symm_inr {α : Type u_2} [inst : LE α] (x : PUnit) :

↑(RelIso.toRelEmbedding (OrderIso.symm WithTop.orderIsoSumLexPUnit)).toEmbedding (↑toLex (Sum.inr x)) = ⊤

source

ink

@[simp]

theorem WithTop.orderIsoSumLexPUnit_symm_inl {α : Type u_1} [inst : LE α] (a : α) :

↑(RelIso.toRelEmbedding (OrderIso.symm WithTop.orderIsoSumLexPUnit)).toEmbedding (↑toLex (Sum.inl a)) = ↑a