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] [IsTrichotomous α 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.

Equations

• RelIso.sumLexComplLeft r x = { toEquiv := Equiv.sumCompl fun (x_1 : α) => r x_1 x, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.sumLexComplLeft_apply {α : Type u_1} {r : α → α → Prop} {x : α} [IsTrans α r] [IsTrichotomous α 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] [IsTrichotomous α 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] [IsTrichotomous α 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.

Equations

• RelIso.sumLexComplRight r x = { toEquiv := (Equiv.sumComm { x_1 : α // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x)), map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.sumLexComplRight_apply {α : Type u_1} {r : α → α → Prop} {x : α} [IsTrans α r] [IsTrichotomous α 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] [IsTrichotomous α 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.

Equations

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

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

Equations

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

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

Equations

• Prod.Lex.prodUnique α β = { toFun := fun (x : Lex (α × β)) => (ofLex x).1, invFun := fun (x : α) => toLex (x, default), left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

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

Equations

• Prod.Lex.uniqueProd α β = { toFun := fun (x : Lex (α × β)) => (ofLex x).2, invFun := fun (x : β) => toLex (default, x), left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

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