Lexicographic order #

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

This file defines the lexicographic relation for pairs of orders, partial orders and linear orders.

Main declarations #

prod.lex.<pre/partial_/linear_>order: Instances lifting the orders on α and β to α ×ₗ β.

Notation #

α ×ₗ β: α × β equipped with the lexicographic order

See also #

Related files are:

data.finset.colex: Colexicographic order on finite sets.
data.list.lex: Lexicographic order on lists.
data.pi.lex: Lexicographic order on Πₗ i, α i.
data.psigma.order: Lexicographic order on Σ' i, α i.
data.sigma.order: Lexicographic order on Σ i, α i.

source

@[protected, instance]

meta def prod.lex.lex.has_to_format {α : Type u_1} {β : Type u_2} [has_to_format α] [has_to_format β] :

has_to_format (α ×ₗ β)

source

@[protected, instance]

def prod.lex.decidable_eq (α : Type u_1) (β : Type u_2) [decidable_eq α] [decidable_eq β] :

decidable_eq (α ×ₗ β)

Equations

prod.lex.decidable_eq α β = prod.decidable_eq

source

@[protected, instance]

def prod.lex.inhabited (α : Type u_1) (β : Type u_2) [inhabited α] [inhabited β] :

inhabited (α ×ₗ β)

Equations

prod.lex.inhabited α β = prod.inhabited

source

@[protected, instance]

def prod.lex.has_le (α : Type u_1) (β : Type u_2) [has_lt α] [has_le β] :

has_le (α ×ₗ β)

Dictionary / lexicographic ordering on pairs.

Equations

prod.lex.has_le α β = {le := prod.lex has_lt.lt has_le.le}

source

@[protected, instance]

def prod.lex.has_lt (α : Type u_1) (β : Type u_2) [has_lt α] [has_lt β] :

has_lt (α ×ₗ β)

Equations

prod.lex.has_lt α β = {lt := prod.lex has_lt.lt has_lt.lt}

source

theorem prod.lex.le_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_le β] (a b : α × β) :

⇑to_lex a ≤ ⇑to_lex b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd ≤ b.snd

source

theorem prod.lex.lt_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] (a b : α × β) :

⇑to_lex a < ⇑to_lex b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd < b.snd

source

@[protected, instance]

def prod.lex.preorder (α : Type u_1) (β : Type u_2) [preorder α] [preorder β] :

preorder (α ×ₗ β)

Dictionary / lexicographic preorder for pairs.

Equations

prod.lex.preorder α β = {le := has_le.le (prod.lex.has_le α β), lt := has_lt.lt (prod.lex.has_lt α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _}

source

theorem prod.lex.to_lex_mono {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] :

monotone ⇑to_lex

source

theorem prod.lex.to_lex_strict_mono {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] :

strict_mono ⇑to_lex

source

@[protected, instance]

def prod.lex.partial_order (α : Type u_1) (β : Type u_2) [partial_order α] [partial_order β] :

partial_order (α ×ₗ β)

Dictionary / lexicographic partial_order for pairs.

Equations

prod.lex.partial_order α β = {le := preorder.le (prod.lex.preorder α β), lt := preorder.lt (prod.lex.preorder α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[protected, instance]

def prod.lex.linear_order (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :

linear_order (α ×ₗ β)

Dictionary / lexicographic linear_order for pairs.

Equations

prod.lex.linear_order α β = {le := partial_order.le (prod.lex.partial_order α β), lt := partial_order.lt (prod.lex.partial_order α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := prod.lex.decidable has_lt.lt has_le.le (λ (a b : β), has_le.le.decidable a b), decidable_eq := prod.lex.decidable_eq α β (λ (a b : β), eq.decidable a b), decidable_lt := prod.lex.decidable has_lt.lt has_lt.lt (λ (a b : β), has_lt.lt.decidable a b), max := max_default (λ (a b : α ×ₗ β), prod.lex.decidable has_lt.lt has_le.le a b), max_def := _, min := min_default (λ (a b : α ×ₗ β), prod.lex.decidable has_lt.lt has_le.le a b), min_def := _}

source

@[protected, instance]

def prod.lex.order_bot {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] [order_bot α] [order_bot β] :

order_bot (α ×ₗ β)

Equations

prod.lex.order_bot = {bot := ⇑to_lex ⊥, bot_le := _}

source

@[protected, instance]

def prod.lex.order_top {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] [order_top α] [order_top β] :

order_top (α ×ₗ β)

Equations

prod.lex.order_top = {top := ⇑to_lex ⊤, le_top := _}

source

@[protected, instance]

def prod.lex.bounded_order {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] [bounded_order α] [bounded_order β] :

bounded_order (α ×ₗ β)

Equations

prod.lex.bounded_order = {top := order_top.top prod.lex.order_top, le_top := _, bot := order_bot.bot prod.lex.order_bot, bot_le := _}

source

@[protected, instance]

def prod.lex.lex.densely_ordered {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [densely_ordered α] [densely_ordered β] :

densely_ordered (α ×ₗ β)

source

@[protected, instance]

def prod.lex.no_max_order_of_left {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [no_max_order α] :

no_max_order (α ×ₗ β)

source

@[protected, instance]

def prod.lex.no_min_order_of_left {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [no_min_order α] :

no_min_order (α ×ₗ β)

source

@[protected, instance]

def prod.lex.no_max_order_of_right {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [no_max_order β] :

no_max_order (α ×ₗ β)

source

@[protected, instance]

def prod.lex.no_min_order_of_right {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [no_min_order β] :

no_min_order (α ×ₗ β)