Lexicographic order and order isomorphisms

Main declarations

• OrderIso.sumLexIioIci and OrderIso.sumLexIicIoi: if α is a linear order and x : α, then α is order isomorphic to both Iio x ⊕ₗ Ici x and Iic x ⊕ₗ Ioi x.
• Prod.Lex.prodUnique and Prod.Lex.uniqueProd: α ×ₗ β is order isomorphic to one side if the other side is Unique.

Relation isomorphism

def RelIso.sumLexComplLeft {α : Type u_1} (r : α → α → Prop) (x : α) [IsTrans α r] [Std.Trichotomous r] [DecidableRel r] : Sum.Lex (Subrel r fun (x_1 : α) => r x_1 x) (Subrel r fun (x_1 : α) => ¬r x_1 x) ≃r r

A relation is isomorphic to the lexicographic sum of elements less than x and elements not less than x.

@[simp]

theorem RelIso.sumLexComplLeft_apply {α : Type u_1} {r : α → α → Prop} {x : α} [IsTrans α r] [Std.Trichotomous r] [DecidableRel r] (a : { x_1 : α // r x_1 x } ⊕ { x_1 : α // ¬r x_1 x }) : (sumLexComplLeft r x) a = (Equiv.sumCompl fun (x_1 : α) => r x_1 x) a

@[simp]

theorem RelIso.sumLexComplLeft_symm_apply {α : Type u_1} {r : α → α → Prop} {x : α} [IsTrans α r] [Std.Trichotomous r] [DecidableRel r] (a : { x_1 : α // r x_1 x } ⊕ { x_1 : α // ¬r x_1 x }) : (sumLexComplLeft r x) a = (Equiv.sumCompl fun (x_1 : α) => r x_1 x) a

def RelIso.sumLexComplRight {α : Type u_1} (r : α → α → Prop) (x : α) [IsTrans α r] [Std.Trichotomous r] [DecidableRel r] : Sum.Lex (Subrel r fun (x_1 : α) => ¬r x x_1) (Subrel r (r x)) ≃r r

A relation is isomorphic to the lexicographic sum of elements not greater than x and elements greater than x.

@[simp]

theorem RelIso.sumLexComplRight_apply {α : Type u_1} {r : α → α → Prop} {x : α} [IsTrans α r] [Std.Trichotomous r] [DecidableRel r] (a : { x_1 : α // ¬r x x_1 } ⊕ Subtype (r x)) : (sumLexComplRight r x) a = (Equiv.sumCompl (r x)) a.swap

@[simp]

theorem RelIso.sumLexComplRight_symm_apply {α : Type u_1} {r : α → α → Prop} {x : α} [IsTrans α r] [Std.Trichotomous r] [DecidableRel r] (a : { x_1 : α // ¬r x x_1 } ⊕ Subtype (r x)) : (sumLexComplRight r x) a = (Equiv.sumCompl (r x)) a.swap

Order isomorphism

def OrderIso.sumLexIioIci {α : Type u_1} [LinearOrder α] (x : α) : Lex (↑(Set.Iio x) ⊕ ↑(Set.Ici x)) ≃o α

A linear order is isomorphic to the lexicographic sum of elements less than x and elements greater or equal to x.

@[simp]

theorem OrderIso.sumLexIioIci_apply_inl {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Iio x)) : (sumLexIioIci x) (toLex (Sum.inl a)) = ↑a

@[simp]

theorem OrderIso.sumLexIioIci_apply_inr {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Ici x)) : (sumLexIioIci x) (toLex (Sum.inr a)) = ↑a

theorem OrderIso.sumLexIioIci_symm_apply_of_lt {α : Type u_1} [LinearOrder α] {x y : α} (h : y < x) : (sumLexIioIci x).symm y = toLex (Sum.inl ⟨y, h⟩)

theorem OrderIso.sumLexIioIci_symm_apply_of_ge {α : Type u_1} [LinearOrder α] {x y : α} (h : x ≤ y) : (sumLexIioIci x).symm y = toLex (Sum.inr ⟨y, h⟩)

@[simp]

theorem OrderIso.sumLexIioIci_symm_apply_Iio {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Iio x)) : (sumLexIioIci x).symm ↑a = toLex (Sum.inl a)

@[simp]

theorem OrderIso.sumLexIioIci_symm_apply_Ici {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Ici x)) : (sumLexIioIci x).symm ↑a = toLex (Sum.inr a)

def OrderIso.sumLexIicIoi {α : Type u_1} [LinearOrder α] (x : α) : Lex (↑(Set.Iic x) ⊕ ↑(Set.Ioi x)) ≃o α

A linear order is isomorphic to the lexicographic sum of elements less or equal to x and elements greater than x.

@[simp]

theorem OrderIso.sumLexIicIoi_apply_inl {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Iic x)) : (sumLexIicIoi x) (toLex (Sum.inl a)) = ↑a

@[simp]

theorem OrderIso.sumLexIicIoi_apply_inr {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Ioi x)) : (sumLexIicIoi x) (toLex (Sum.inr a)) = ↑a

theorem OrderIso.sumLexIicIoi_symm_apply_of_le {α : Type u_1} [LinearOrder α] {x y : α} (h : y ≤ x) : (sumLexIicIoi x).symm y = toLex (Sum.inl ⟨y, h⟩)

theorem OrderIso.sumLexIicIoi_symm_apply_of_lt {α : Type u_1} [LinearOrder α] {x y : α} (h : x < y) : (sumLexIicIoi x).symm y = toLex (Sum.inr ⟨y, h⟩)

@[simp]

theorem OrderIso.sumLexIicIoi_symm_apply_Iic {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Iic x)) : (sumLexIicIoi x).symm ↑a = Sum.inl a

@[simp]

theorem OrderIso.sumLexIicIoi_symm_apply_Ioi {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Ioi x)) : (sumLexIicIoi x).symm ↑a = Sum.inr a

Degenerate products

def Prod.Lex.prodUnique (α : Type u_2) (β : Type u_3) [PartialOrder α] [Preorder β] [Unique β] : Lex (α × β) ≃o α

Lexicographic product type with Unique type on the right is OrderIso to the left.

@[simp]

theorem Prod.Lex.prodUnique_apply {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Unique β] (x : Lex (α × β)) : (prodUnique α β) x = (ofLex x).1

def Prod.Lex.uniqueProd (α : Type u_2) (β : Type u_3) [Preorder α] [Unique α] [LE β] : Lex (α × β) ≃o β

Lexicographic product type with Unique type on the left is OrderIso to the right.

@[simp]

theorem Prod.Lex.uniqueProd_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Unique α] [LE β] (x : Lex (α × β)) : (uniqueProd α β) x = (ofLex x).2

def Prod.Lex.prodLexAssoc (α : Type u_4) (β : Type u_5) (γ : Type u_6) [Preorder α] [Preorder β] [Preorder γ] : Lex (Lex (α × β) × γ) ≃o Lex (α × Lex (β × γ))

Equiv.prodAssoc promoted to an order isomorphism of lexicographic products.

@[simp]

theorem Prod.Lex.prodLexAssoc_symm_apply (α : Type u_4) (β : Type u_5) (γ : Type u_6) [Preorder α] [Preorder β] [Preorder γ] (a✝ : Lex (α × Lex (β × γ))) : (RelIso.symm (prodLexAssoc α β γ)) a✝ = toLex (toLex ((ofLex a✝).1, (ofLex (ofLex a✝).2).1), (ofLex (ofLex a✝).2).2)

@[simp]

theorem Prod.Lex.prodLexAssoc_apply (α : Type u_4) (β : Type u_5) (γ : Type u_6) [Preorder α] [Preorder β] [Preorder γ] (a✝ : Lex (Lex (α × β) × γ)) : (prodLexAssoc α β γ) a✝ = toLex ((ofLex (ofLex a✝).1).1, toLex ((ofLex (ofLex a✝).1).2, (ofLex a✝).2))

def Prod.Lex.sumLexProdLexDistrib (α : Type u_4) (β : Type u_5) (γ : Type u_6) [Preorder α] [Preorder β] [Preorder γ] : Lex (Lex (α ⊕ β) × γ) ≃o Lex (Lex (α × γ) ⊕ Lex (β × γ))

Equiv.sumProdDistrib promoted to an order isomorphism of lexicographic products.

Right distributivity doesn't hold. A counterexample is ℕ ×ₗ (Unit ⊕ₗ Unit) ≃o ℕ which is not isomorphic to ℕ ×ₗ Unit ⊕ₗ ℕ ×ₗ Unit ≃o ℕ ⊕ₗ ℕ.

@[simp]

theorem Prod.Lex.sumLexProdLexDistrib_symm_apply (α : Type u_4) (β : Type u_5) (γ : Type u_6) [Preorder α] [Preorder β] [Preorder γ] (a✝ : Lex (Lex (α × γ) ⊕ Lex (β × γ))) : (RelIso.symm (sumLexProdLexDistrib α β γ)) a✝ = toLex (map (⇑toLex) id ((Equiv.sumProdDistrib α β γ).symm (Sum.map (⇑ofLex) (⇑ofLex) (ofLex a✝))))

@[simp]

theorem Prod.Lex.sumLexProdLexDistrib_apply (α : Type u_4) (β : Type u_5) (γ : Type u_6) [Preorder α] [Preorder β] [Preorder γ] (a✝ : Lex (Lex (α ⊕ β) × γ)) : (sumLexProdLexDistrib α β γ) a✝ = toLex (Sum.map (⇑toLex) (⇑toLex) ((Equiv.sumProdDistrib α β γ) (map (⇑ofLex) id (ofLex a✝))))

def Prod.Lex.prodLexCongr {α : Type u_4} {β : Type u_5} {γ : Type u_6} {δ : Type u_7} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (ea : α ≃o β) (eb : γ ≃o δ) : Lex (α × γ) ≃o Lex (β × δ)

Equiv.prodCongr promoted to an order isomorphism between lexicographic products.

@[simp]

theorem Prod.Lex.prodLexCongr_apply {α : Type u_4} {β : Type u_5} {γ : Type u_6} {δ : Type u_7} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (ea : α ≃o β) (eb : γ ≃o δ) (a✝ : Lex (α × γ)) : (prodLexCongr ea eb) a✝ = toLex (map (⇑ea) (⇑eb) (ofLex a✝))