data.sum.order

# Orders on a sum type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the disjoint sum and the linear (aka lexicographic) sum of two orders and provides relation instances for sum.lift_rel 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.has_le, sum.has_lt: Disjoint sum of orders.
• sum.lex.has_le, sum.lex.has_lt: Lexicographic/linear sum of orders.

## Notation #

• α ⊕ₗ β: The linear sum of α and β.

### Unbundled relation classes #

@[refl]
theorem sum.lift_rel.refl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] (x : α β) :
s x x
@[protected, instance]
def sum.lift_rel.is_refl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] :
is_refl β) s)
@[protected, instance]
def sum.lift_rel.is_irrefl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] :
is_irrefl β) s)
@[trans]
theorem sum.lift_rel.trans {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] {a b c : α β} :
s a b s b c s a c
@[protected, instance]
def sum.lift_rel.is_trans {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] :
is_trans β) s)
@[protected, instance]
def sum.lift_rel.is_antisymm {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] :
is_antisymm β) s)
@[protected, instance]
def sum.lex.is_refl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] :
is_refl β) (sum.lex r s)
@[protected, instance]
def sum.lex.is_irrefl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] :
is_irrefl β) (sum.lex r s)
@[protected, instance]
def sum.lex.is_trans {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] :
is_trans β) (sum.lex r s)
@[protected, instance]
def sum.lex.is_antisymm {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] :
is_antisymm β) (sum.lex r s)
@[protected, instance]
def sum.lex.is_total {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] :
is_total β) (sum.lex r s)
@[protected, instance]
def sum.lex.is_trichotomous {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] :
@[protected, instance]
def sum.lex.is_well_order {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] :
is_well_order β) (sum.lex r s)

### Disjoint sum of two orders #

@[protected, instance]
def sum.has_le {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] :
has_le β)
Equations
@[protected, instance]
def sum.has_lt {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] :
has_lt β)
Equations
theorem sum.le_def {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α β} :
a b
theorem sum.lt_def {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α β} :
a < b
@[simp]
theorem sum.inl_le_inl_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α} :
a b
@[simp]
theorem sum.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : β} :
a b
@[simp]
theorem sum.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α} :
< a < b
@[simp]
theorem sum.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : β} :
< a < b
@[simp]
theorem sum.not_inl_le_inr {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a : α} {b : β} :
@[simp]
theorem sum.not_inl_lt_inr {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a : α} {b : β} :
¬ <
@[simp]
theorem sum.not_inr_le_inl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a : α} {b : β} :
@[simp]
theorem sum.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a : α} {b : β} :
¬ <
@[protected, instance]
def sum.preorder {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
preorder β)
Equations
theorem sum.inl_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
theorem sum.inr_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
theorem sum.inl_strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
theorem sum.inr_strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
@[protected, instance]
def sum.partial_order {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def sum.no_min_order {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [no_min_order α] [no_min_order β] :
@[protected, instance]
def sum.no_max_order {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [no_max_order α] [no_max_order β] :
@[simp]
theorem sum.no_min_order_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] :
@[simp]
theorem sum.no_max_order_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] :
@[protected, instance]
def sum.densely_ordered {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β]  :
@[simp]
theorem sum.densely_ordered_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] :
@[simp]
theorem sum.swap_le_swap_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α β} :
a.swap b.swap a b
@[simp]
theorem sum.swap_lt_swap_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α β} :
a.swap < b.swap a < b

### Linear sum of two orders #

@[reducible]
def sum.inlₗ {α : Type u_1} {β : Type u_2} (x : α) :
α ⊕ₗ β

Lexicographical sum.inl. Only used for pattern matching.

@[reducible]
def sum.inrₗ {α : Type u_1} {β : Type u_2} (x : β) :
α ⊕ₗ β

Lexicographical sum.inr. Only used for pattern matching.

@[protected, instance]
def sum.lex.has_le {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] :
has_le ⊕ₗ β)

The linear/lexicographical ≤ on a sum.

Equations
@[protected, instance]
def sum.lex.has_lt {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] :
has_lt ⊕ₗ β)

The linear/lexicographical < on a sum.

Equations
@[simp]
theorem sum.lex.to_lex_le_to_lex {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α β} :
@[simp]
theorem sum.lex.to_lex_lt_to_lex {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α β} :
<
theorem sum.lex.le_def {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α ⊕ₗ β} :
a b (of_lex b)
theorem sum.lex.lt_def {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α ⊕ₗ β} :
a < b (of_lex b)
@[simp]
theorem sum.lex.inl_le_inl_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α} :
@[simp]
theorem sum.lex.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : β} :
@[simp]
theorem sum.lex.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α} :
@[simp]
theorem sum.lex.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : β} :
@[simp]
theorem sum.lex.inl_le_inr {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (a : α) (b : β) :
@[simp]
theorem sum.lex.inl_lt_inr {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] (a : α) (b : β) :
@[simp]
theorem sum.lex.not_inr_le_inl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a : α} {b : β} :
@[simp]
theorem sum.lex.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a : α} {b : β} :
@[protected, instance]
def sum.lex.preorder {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
Equations
theorem sum.lex.to_lex_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
theorem sum.lex.to_lex_strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
theorem sum.lex.inl_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
theorem sum.lex.inr_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
theorem sum.lex.inl_strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
theorem sum.lex.inr_strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
@[protected, instance]
def sum.lex.partial_order {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def sum.lex.linear_order {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] :
Equations
@[protected, instance]
def sum.lex.order_bot {α : Type u_1} {β : Type u_2} [has_le α] [order_bot α] [has_le β] :

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

Equations
@[simp]
theorem sum.lex.inl_bot {α : Type u_1} {β : Type u_2} [has_le α] [order_bot α] [has_le β] :
@[protected, instance]
def sum.lex.order_top {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] [order_top β] :

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

Equations
@[simp]
theorem sum.lex.inr_top {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] [order_top β] :
@[protected, instance]
def sum.lex.bounded_order {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] [order_bot α] [order_top β] :
Equations
@[protected, instance]
def sum.lex.no_min_order {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [no_min_order α] [no_min_order β] :
@[protected, instance]
def sum.lex.no_max_order {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [no_max_order α] [no_max_order β] :
@[protected, instance]
def sum.lex.no_min_order_of_nonempty {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [no_min_order α] [nonempty α] :
@[protected, instance]
def sum.lex.no_max_order_of_nonempty {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] [no_max_order β] [nonempty β] :
@[protected, instance]
@[protected, instance]

### Order isomorphisms #

def order_iso.sum_comm (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :
α β ≃o β α

equiv.sum_comm promoted to an order isomorphism.

Equations
@[simp]
theorem order_iso.sum_comm_apply (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] (ᾰ : α β) :
β) = β).to_fun
@[simp]
theorem order_iso.sum_comm_symm (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :
β).symm =
def order_iso.sum_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) [has_le α] [has_le β] [has_le γ] :
β) γ ≃o α β γ

equiv.sum_assoc promoted to an order isomorphism.

Equations
@[simp]
theorem order_iso.sum_assoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (a : α) :
γ) (sum.inl (sum.inl a)) =
@[simp]
theorem order_iso.sum_assoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (b : β) :
@[simp]
theorem order_iso.sum_assoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (c : γ) :
@[simp]
theorem order_iso.sum_assoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (a : α) :
β γ).symm) (sum.inl a) = sum.inl (sum.inl a)
@[simp]
theorem order_iso.sum_assoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (b : β) :
β γ).symm) (sum.inr (sum.inl b)) = sum.inl (sum.inr b)
@[simp]
theorem order_iso.sum_assoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (c : γ) :
β γ).symm) (sum.inr (sum.inr c)) =
def order_iso.sum_dual_distrib (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :

order_dual is distributive over ⊕ up to an order isomorphism.

Equations
@[simp]
theorem order_iso.sum_dual_distrib_inl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (a : α) :
@[simp]
theorem order_iso.sum_dual_distrib_inr {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (b : β) :
@[simp]
theorem order_iso.sum_dual_distrib_symm_inl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (a : α) :
@[simp]
theorem order_iso.sum_dual_distrib_symm_inr {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (b : β) :
def order_iso.sum_lex_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) [has_le α] [has_le β] [has_le γ] :
⊕ₗ β) ⊕ₗ γ ≃o α ⊕ₗ β ⊕ₗ γ

equiv.sum_assoc promoted to an order isomorphism.

Equations
@[simp]
theorem order_iso.sum_lex_assoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (a : α) :
@[simp]
theorem order_iso.sum_lex_assoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (b : β) :
@[simp]
theorem order_iso.sum_lex_assoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (c : γ) :
@[simp]
theorem order_iso.sum_lex_assoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (a : α) :
@[simp]
theorem order_iso.sum_lex_assoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (b : β) :
@[simp]
theorem order_iso.sum_lex_assoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (c : γ) :
γ).symm) (sum.inr (sum.inr c)) =
def order_iso.sum_lex_dual_antidistrib (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :

order_dual is antidistributive over ⊕ₗ up to an order isomorphism.

Equations
@[simp]
theorem order_iso.sum_lex_dual_antidistrib_inl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (a : α) :
@[simp]
theorem order_iso.sum_lex_dual_antidistrib_inr {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (b : β) :
@[simp]
theorem order_iso.sum_lex_dual_antidistrib_symm_inl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (b : β) :
@[simp]
theorem order_iso.sum_lex_dual_antidistrib_symm_inr {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (a : α) :

with_bot α is order-isomorphic to punit ⊕ₗ α, by sending ⊥ to punit.star and ↑a to a.

Equations
@[simp]
theorem with_bot.order_iso_punit_sum_lex_bot {α : Type u_1} [has_le α] :
= to_lex (sum.inl punit.star)
@[simp]
theorem with_bot.order_iso_punit_sum_lex_coe {α : Type u_1} [has_le α] (a : α) :
@[simp]
theorem with_bot.order_iso_punit_sum_lex_symm_inl {α : Type u_1} [has_le α] (x : punit) :
@[simp]
theorem with_bot.order_iso_punit_sum_lex_symm_inr {α : Type u_1} [has_le α] (a : α) :

with_top α is order-isomorphic to α ⊕ₗ punit, by sending ⊤ to punit.star and ↑a to a.

Equations
@[simp]
theorem with_top.order_iso_sum_lex_punit_top {α : Type u_1} [has_le α] :
= to_lex (sum.inr punit.star)
@[simp]
theorem with_top.order_iso_sum_lex_punit_coe {α : Type u_1} [has_le α] (a : α) :
@[simp]
theorem with_top.order_iso_sum_lex_punit_symm_inr {α : Type u_1} [has_le α] (x : punit) :
@[simp]
theorem with_top.order_iso_sum_lex_punit_symm_inl {α : Type u_1} [has_le α] (a : α) :