mathlib documentation

order.lexicographic

Lexicographic order #

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

Main declarations #

See also #

Related files are:

source
def lex (α : Type u) (β : Type v) :
Type (max u v)

The cartesian product, equipped with the lexicographic order.

Equations
source
@[protected, instance]
meta def lex.has_to_format {α : Type u} {β : Type v} [has_to_format α] [has_to_format β] :
has_to_format (lex α β)
source
@[protected, instance]
def lex.decidable_eq {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] :
decidable_eq (lex α β)
Equations
source
@[protected, instance]
def lex.inhabited {α : Type u} {β : Type v} [inhabited α] [inhabited β] :
inhabited (lex α β)
Equations
source
@[protected, instance]
def lex_has_le {α : Type u} {β : Type v} [has_lt α] [has_le β] :
has_le (lex α β)

Dictionary / lexicographic ordering on pairs.

Equations
source
@[protected, instance]
def lex_has_lt {α : Type u} {β : Type v} [has_lt α] [has_lt β] :
has_lt (lex α β)
Equations
source
theorem lex_le_iff {α : Type u} {β : Type v} [has_lt α] [has_le β] (a b : lex α β) :
a ≤ b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd ≤ b.snd
source
theorem lex_lt_iff {α : Type u} {β : Type v} [has_lt α] [has_lt β] (a b : lex α β) :
a < b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd < b.snd
source
@[protected, instance]
def lex_preorder {α : Type u} {β : Type v} [preorder α] [preorder β] :
preorder (lex α β)

Dictionary / lexicographic preorder for pairs.

Equations
source
@[protected, instance]
def lex_partial_order {α : Type u} {β : Type v} [partial_order α] [partial_order β] :
partial_order (lex α β)

Dictionary / lexicographic partial_order for pairs.

Equations
source
@[protected, instance]
def lex_linear_order {α : Type u} {β : Type v} [linear_order α] [linear_order β] :
linear_order (lex α β)

Dictionary / lexicographic linear_order for pairs.

Equations