mathlib3 documentation

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 #

Notation #

Unbundled relation classes #

@[refl]
theorem sum.lift_rel.refl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_refl α r] [is_refl β s] (x : α β) :
sum.lift_rel r s x x
@[protected, instance]
def sum.lift_rel.is_refl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_refl α r] [is_refl β s] :
is_refl β) (sum.lift_rel r s)
@[protected, instance]
def sum.lift_rel.is_irrefl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_irrefl α r] [is_irrefl β s] :
is_irrefl β) (sum.lift_rel r s)
@[trans]
theorem sum.lift_rel.trans {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_trans α r] [is_trans β s] {a b c : α β} :
sum.lift_rel r s a b sum.lift_rel r s b c sum.lift_rel r s a c
@[protected, instance]
def sum.lift_rel.is_trans {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_trans α r] [is_trans β s] :
is_trans β) (sum.lift_rel r s)
@[protected, instance]
def sum.lift_rel.is_antisymm {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_antisymm α r] [is_antisymm β s] :
@[protected, instance]
def sum.lex.is_refl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_refl α r] [is_refl β s] :
is_refl β) (sum.lex r s)
@[protected, instance]
def sum.lex.is_irrefl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_irrefl α r] [is_irrefl β s] :
is_irrefl β) (sum.lex r s)
@[protected, instance]
def sum.lex.is_trans {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_trans α r] [is_trans β s] :
is_trans β) (sum.lex r s)
@[protected, instance]
def sum.lex.is_antisymm {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_antisymm α r] [is_antisymm β s] :
is_antisymm β) (sum.lex r s)
@[protected, instance]
def sum.lex.is_total {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_total α r] [is_total β s] :
is_total β) (sum.lex r s)
@[protected, instance]
def sum.lex.is_trichotomous {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_trichotomous α r] [is_trichotomous β s] :
@[protected, instance]
def sum.lex.is_well_order {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_well_order α r] [is_well_order β 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 : α β} :
theorem sum.lt_def {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α β} :
@[simp]
theorem sum.inl_le_inl_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : α} :
@[simp]
theorem sum.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {a b : β} :
@[simp]
theorem sum.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a b : α} :
@[simp]
theorem sum.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {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} [partial_order α] [partial_order β] :
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 β] [densely_ordered α] [densely_ordered β] :
@[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 : α ⊕ₗ β} :
theorem sum.lex.lt_def {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] {a 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.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 β] (ᾰ : α β) :
@[simp]
theorem order_iso.sum_comm_symm (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :
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 : α) :
@[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 : α) :
@[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 : β) :
@[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 : γ) :
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
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 : γ) :
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

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

Equations

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

Equations