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

theorem Sum.LiftRel.refl {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Refl r] [Std.Refl s] (x : α ⊕ β) :

LiftRel r s x x

source

instance Sum.instReflLiftRel_mathlib {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Refl r] [Std.Refl s] :

Std.Refl (LiftRel r s)

source

instance Sum.instIrreflLiftRel_mathlib {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Irrefl r] [Std.Irrefl s] :

Std.Irrefl (LiftRel r s)

source

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

source

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

IsTrans (α ⊕ β) (LiftRel r s)

source

instance Sum.instAntisymmLiftRel_mathlib {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Antisymm r] [Std.Antisymm s] :

Std.Antisymm (LiftRel r s)

source

instance Sum.instReflLex_mathlib {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Refl r] [Std.Refl s] :

Std.Refl (Lex r s)

source

instance Sum.instIrreflLex_mathlib {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Irrefl r] [Std.Irrefl s] :

Std.Irrefl (Lex r s)

source

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

IsTrans (α ⊕ β) (Lex r s)

source

instance Sum.instAntisymmLex_mathlib {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Antisymm r] [Std.Antisymm s] :

Std.Antisymm (Lex r s)

source

instance Sum.instTotalLex_mathlib {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Total r] [Std.Total s] :

Std.Total (Lex r s)

source

instance Sum.instTrichotomousLex_mathlib {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Trichotomous r] [Std.Trichotomous s] :

Std.Trichotomous (Lex r s)

source

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

IsWellOrder (α ⊕ β) (Lex r s)

source

theorem Sum.lex_flip_iff {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (a b : α ⊕ β) :

Lex (flip r) (flip s) a b ↔ Lex s r b.swap a.swap

Disjoint sum of two orders #

source

@[instance_reducible]

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

LE (α ⊕ β)

source

@[instance_reducible]

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

LT (α ⊕ β)

source

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

source

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

source

@[simp]

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

inl a ≤ inl b ↔ a ≤ b

source

@[simp]

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

inr a ≤ inr b ↔ a ≤ b

source

@[simp]

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

inl a < inl b ↔ a < b

source

@[simp]

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

inr a < inr b ↔ a < b

source

@[simp]

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

¬inl b ≤ inr a

source

@[simp]

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

¬inl b < inr a

source

@[simp]

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

¬inr b ≤ inl a

source

@[simp]

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

¬inr b < inl a

source

@[instance_reducible]

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

Preorder (α ⊕ β)

source

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

Monotone inl

source

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

Monotone inr

source

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

StrictMono inl

source

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

StrictMono inr

source

@[instance_reducible]

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

PartialOrder (α ⊕ β)

source

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

NoMinOrder (α ⊕ β)

source

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

NoMaxOrder (α ⊕ β)

source

@[simp]

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

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

source

@[simp]

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

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

source

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

DenselyOrdered (α ⊕ β)

source

@[simp]

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

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

source

@[simp]

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

a.swap ≤ b.swap ↔ a ≤ b

source

@[simp]

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

a.swap < b.swap ↔ a < b

source

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

Monotone swap

source

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

StrictMono swap

Linear sum of two orders #

source

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

Lean.TrailingParserDescr

The linear sum of two orders

Instances For

source

@[reducible, match_pattern, inline]

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

α ⊕ₗ β

Lexicographical Sum.inl. Only used for pattern matching.

Instances For

source

@[reducible, match_pattern, inline]

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

α ⊕ₗ β

Lexicographical Sum.inr. Only used for pattern matching.

Instances For

source

@[instance_reducible]

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

LE (α ⊕ₗ β)

The linear/lexicographical ≤ on a sum.

source

@[instance_reducible]

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

LT (α ⊕ₗ β)

The linear/lexicographical < on a sum.

source

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

source

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

source

theorem Sum.Lex.le_def {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : α ⊕ₗ β} :

a ≤ b ↔ Lex (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) (ofLex a) (ofLex b)

source

theorem Sum.Lex.lt_def {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : α ⊕ₗ β} :

a < b ↔ Lex (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : β) => x1 < x2) (ofLex a) (ofLex b)

source

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

source

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

source

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

source

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

source

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

toLex (inl a) ≤ toLex (inr b)

source

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

toLex (inl a) < toLex (inr b)

source

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

¬toLex (inr b) ≤ toLex (inl a)

source

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

¬toLex (inr b) < toLex (inl a)

source

def Sum.Lex.toLexRelIsoLT {α : Type u_1} {β : Type u_2} [LT α] [LT β] :

(Lex (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) ≃r fun (x1 x2 : α ⊕ₗ β) => x1 < x2

toLex promoted to a RelIso between < relations.

Instances For

source

@[simp]

theorem Sum.Lex.toLexRelIsoLT_coe {α : Type u_1} {β : Type u_2} [LT α] [LT β] :

⇑toLexRelIsoLT = ⇑toLex

source

@[simp]

theorem Sum.Lex.toLexRelIsoLT_symm_coe {α : Type u_1} {β : Type u_2} [LT α] [LT β] :

⇑toLexRelIsoLT.symm = ⇑ofLex

source

def Sum.Lex.toLexRelIsoLE {α : Type u_1} {β : Type u_2} [LE α] [LE β] :

(Lex (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : β) => x1 ≤ x2) ≃r fun (x1 x2 : α ⊕ₗ β) => x1 ≤ x2

toLex promoted to a RelIso between ≤ relations.

Instances For

source

@[simp]

theorem Sum.Lex.toLexRelIsoLE_coe {α : Type u_1} {β : Type u_2} [LE α] [LE β] :

⇑toLexRelIsoLE = ⇑toLex

source

@[simp]

theorem Sum.Lex.toLexRelIsoLE_symm_coe {α : Type u_1} {β : Type u_2} [LE α] [LE β] :

⇑toLexRelIsoLE.symm = ⇑ofLex

source

@[instance_reducible]

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

Preorder (α ⊕ₗ β)

source

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

Monotone ⇑toLex

source

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

StrictMono ⇑toLex

source

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

Monotone (⇑toLex ∘ inl)

source

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

Monotone (⇑toLex ∘ inr)

source

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

StrictMono (⇑toLex ∘ inl)

source

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

StrictMono (⇑toLex ∘ inr)

source

@[instance_reducible]

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

PartialOrder (α ⊕ₗ β)

source

@[instance_reducible]

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

LinearOrder (α ⊕ₗ β)

source

@[instance_reducible]

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

OrderBot (α ⊕ₗ β)

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

source

@[simp]

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

toLex (inl ⊥) = ⊥

source

@[instance_reducible]

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

OrderTop (α ⊕ₗ β)

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

source

@[simp]

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

toLex (inr ⊤) = ⊤

source

@[instance_reducible]

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

BoundedOrder (α ⊕ₗ β)

source

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

NoMinOrder (α ⊕ₗ β)

source

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

NoMaxOrder (α ⊕ₗ β)

source

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

NoMinOrder (α ⊕ₗ β)

source

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

NoMaxOrder (α ⊕ₗ β)

source

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

DenselyOrdered (α ⊕ₗ β)

source

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

DenselyOrdered (α ⊕ₗ β)

source

instance Sum.Lex.instWellFoundedLTLex {α : Type u_1} {β : Type u_2} [LT α] [LT β] [WellFoundedLT α] [WellFoundedLT β] :

WellFoundedLT (α ⊕ₗ β)

source

instance Sum.Lex.instWellFoundedGTLex {α : Type u_1} {β : Type u_2} [LT α] [LT β] [WellFoundedGT α] [WellFoundedGT β] :

WellFoundedGT (α ⊕ₗ β)

Order isomorphisms #

source

def OrderIso.sumCongr {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [LE α₁] [LE α₂] [LE β₁] [LE β₂] (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂) :

α₁ ⊕ β₁ ≃o α₂ ⊕ β₂

Equiv.sumCongr promoted to an order isomorphism.

Instances For

source

@[simp]

theorem OrderIso.sumCongr_apply {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [LE α₁] [LE α₂] [LE β₁] [LE β₂] (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂) (a✝ : α₁ ⊕ β₁) :

(ea.sumCongr eb) a✝ = Sum.map (⇑ea) (⇑eb) a✝

source

@[simp]

theorem OrderIso.sumCongr_trans {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} {γ₁ : Type u_8} {γ₂ : Type u_9} [LE α₁] [LE α₂] [LE β₁] [LE β₂] [LE γ₁] [LE γ₂] (e₁ : α₁ ≃o β₁) (e₂ : α₂ ≃o β₂) (f₁ : β₁ ≃o γ₁) (f₂ : β₂ ≃o γ₂) :

(e₁.sumCongr e₂).trans (f₁.sumCongr f₂) = (e₁.trans f₁).sumCongr (e₂.trans f₂)

source

@[simp]

theorem OrderIso.sumCongr_symm {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [LE α₁] [LE α₂] [LE β₁] [LE β₂] (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂) :

(ea.sumCongr eb).symm = ea.symm.sumCongr eb.symm

source

@[simp]

theorem OrderIso.sumCongr_refl {α : Type u_1} {β : Type u_2} [LE α] [LE β] :

(refl α).sumCongr (refl β) = refl (α ⊕ β)

source

def OrderIso.sumComm (α : Type u_10) (β : Type u_11) [LE α] [LE β] :

α ⊕ β ≃o β ⊕ α

Equiv.sumComm promoted to an order isomorphism.

Instances For

source

@[simp]

theorem OrderIso.sumComm_apply (α : Type u_10) (β : Type u_11) [LE α] [LE β] (a✝ : α ⊕ β) :

(sumComm α β) a✝ = a✝.swap

source

@[simp]

theorem OrderIso.sumComm_symm (α : Type u_10) (β : Type u_11) [LE α] [LE β] :

(sumComm α β).symm = sumComm β α

source

def OrderIso.sumAssoc (α : Type u_10) (β : Type u_11) (γ : Type u_12) [LE α] [LE β] [LE γ] :

(α ⊕ β) ⊕ γ ≃o α ⊕ β ⊕ γ

Equiv.sumAssoc promoted to an order isomorphism.

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

def OrderIso.sumDualDistrib (α : Type u_10) (β : Type u_11) [LE α] [LE β] :

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

orderDual is distributive over ⊕ up to an order isomorphism.

Instances For

source

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

source

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

source

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

source

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

source

def OrderIso.sumLexCongr {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [LE α₁] [LE α₂] [LE β₁] [LE β₂] (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂) :

α₁ ⊕ₗ β₁ ≃o α₂ ⊕ₗ β₂

Equiv.sumCongr promoted to an order isomorphism between lexicographic sums.

Instances For

source

@[simp]

theorem OrderIso.sumLexCongr_apply {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [LE α₁] [LE α₂] [LE β₁] [LE β₂] (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂) (a✝ : α₁ ⊕ₗ β₁) :

(ea.sumLexCongr eb) a✝ = toLex (Sum.map (⇑ea) (⇑eb) (ofLex a✝))

source

@[simp]

theorem OrderIso.sumLexCongr_trans {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} {γ₁ : Type u_8} {γ₂ : Type u_9} [LE α₁] [LE α₂] [LE β₁] [LE β₂] [LE γ₁] [LE γ₂] (e₁ : α₁ ≃o β₁) (e₂ : α₂ ≃o β₂) (f₁ : β₁ ≃o γ₁) (f₂ : β₂ ≃o γ₂) :

(e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂) = (e₁.trans f₁).sumLexCongr (e₂.trans f₂)

source

@[simp]

theorem OrderIso.sumLexCongr_symm {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [LE α₁] [LE α₂] [LE β₁] [LE β₂] (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂) :