mathlib documentation

data.prod.lex

Lexicographic order #

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

Main declarations #

Notation #

See also #

Related files are:

@[protected, instance]
meta def prod.lex.lex.has_to_format {α : Type u_1} {β : Type u_2} [has_to_format α] [has_to_format β] :
@[protected, instance]
def prod.lex.decidable_eq (α : Type u_1) (β : Type u_2) [decidable_eq α] [decidable_eq β] :
Equations
@[protected, instance]
def prod.lex.inhabited (α : Type u_1) (β : Type u_2) [inhabited α] [inhabited β] :
Equations
@[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
@[protected, instance]
def prod.lex.has_lt (α : Type u_1) (β : Type u_2) [has_lt α] [has_lt β] :
has_lt ×ₗ β)
Equations
theorem prod.lex.le_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_le β] (a b : α × β) :
theorem prod.lex.lt_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] (a b : α × β) :
@[protected, instance]
def prod.lex.preorder (α : Type u_1) (β : Type u_2) [preorder α] [preorder β] :
preorder ×ₗ β)

Dictionary / lexicographic preorder for pairs.

Equations
@[protected, instance]
def prod.lex.partial_order (α : Type u_1) (β : Type u_2) [partial_order α] [partial_order β] :

Dictionary / lexicographic partial_order for pairs.

Equations
@[protected, instance]
def prod.lex.linear_order (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :

Dictionary / lexicographic linear_order for pairs.

Equations