mathlib3 documentation

data.prod.lex

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 #

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
theorem prod.lex.to_lex_mono {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] :
@[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
@[protected, instance]
def prod.lex.order_bot {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] [order_bot α] [order_bot β] :
Equations
@[protected, instance]
def prod.lex.order_top {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] [order_top α] [order_top β] :
Equations
@[protected, instance]
@[protected, instance]
def prod.lex.no_max_order_of_left {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [no_max_order α] :
@[protected, instance]
def prod.lex.no_min_order_of_left {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [no_min_order α] :
@[protected, instance]
def prod.lex.no_max_order_of_right {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [no_max_order β] :
@[protected, instance]
def prod.lex.no_min_order_of_right {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [no_min_order β] :