Lexicographic order and order isomorphisms #
Main declarations #
OrderIso.sumLexIioIciandOrderIso.sumLexIicIoi: ifαis a linear order andx : α, thenαis order isomorphic to bothIio x ⊕ₗ Ici xandIic x ⊕ₗ Ioi x.Prod.Lex.prodUniqueandProd.Lex.uniqueProd:α ×ₗ βis order isomorphic to one side if the other side isUnique.
Relation isomorphism #
def
RelIso.sumLexComplLeft
{α : Type u_1}
(r : α → α → Prop)
(x : α)
[IsTrans α r]
[Std.Trichotomous r]
[DecidableRel r]
:
A relation is isomorphic to the lexicographic sum of elements less than x and elements not
less than x.
Instances For
@[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]
:
A relation is isomorphic to the lexicographic sum of elements not greater than x and elements
greater than x.
Instances For
@[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 #
A linear order is isomorphic to the lexicographic sum of elements less than x and elements
greater or equal to x.
Instances For
@[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)
A linear order is isomorphic to the lexicographic sum of elements less or equal to x and
elements greater than x.
Instances For
@[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 #
Lexicographic product type with Unique type on the right is OrderIso to the left.
Instances For
@[simp]
theorem
Prod.Lex.prodUnique_apply
{α : Type u_2}
{β : Type u_3}
[PartialOrder α]
[Preorder β]
[Unique β]
(x : Lex (α × β))
:
(prodUnique α β) x = (ofLex x).1
@[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 γ]
:
Equiv.prodAssoc promoted to an order isomorphism of lexicographic products.
Instances For
@[simp]
def
Prod.Lex.sumLexProdLexDistrib
(α : Type u_4)
(β : Type u_5)
(γ : Type u_6)
[Preorder α]
[Preorder β]
[Preorder γ]
:
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 ℕ ⊕ₗ ℕ.
Instances For
@[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]