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

source
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' := ⋯ }

Instances For

source
@[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
source
@[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
source
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' := ⋯ }

Instances For

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

source
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.

Instances For

source
@[simp]
theorem OrderIso.sumLexIioIci_apply_inl {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Iio x)) :
(sumLexIioIci x) (toLex (Sum.inl a)) = ↑a
source
@[simp]
theorem OrderIso.sumLexIioIci_apply_inr {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Ici x)) :
(sumLexIioIci x) (toLex (Sum.inr a)) = ↑a
source
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⟩)
source
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⟩)
source
@[simp]
theorem OrderIso.sumLexIioIci_symm_apply_Iio {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Iio x)) :
(sumLexIioIci x).symm ↑a = toLex (Sum.inl a)
source
@[simp]
theorem OrderIso.sumLexIioIci_symm_apply_Ici {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Ici x)) :
(sumLexIioIci x).symm ↑a = toLex (Sum.inr a)
source
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.

Instances For

source
@[simp]
theorem OrderIso.sumLexIicIoi_apply_inl {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Iic x)) :
(sumLexIicIoi x) (toLex (Sum.inl a)) = ↑a
source
@[simp]
theorem OrderIso.sumLexIicIoi_apply_inr {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Ioi x)) :
(sumLexIicIoi x) (toLex (Sum.inr a)) = ↑a
source
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⟩)
source
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⟩)
source
@[simp]
theorem OrderIso.sumLexIicIoi_symm_apply_Iic {α : Type u_1} [LinearOrder α] {x : α} (a : ↑(Set.Iic x)) :
(sumLexIicIoi x).symm ↑a = Sum.inl a
source
@[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 #

source
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' := ⋯ }

Instances For

source
@[simp]
theorem Prod.Lex.prodUnique_apply {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Unique β] (x : Lex (α × β)) :
(prodUnique α β) x = (ofLex x).1
source
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' := ⋯ }

Instances For

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