Documentation

Mathlib.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:

A type synonym to equip a type with its lexicographic order.

Equations
instance Prod.Lex.decidableEq (α : Type u_1) (β : Type u_2) [inst : DecidableEq α] [inst : DecidableEq β] :
DecidableEq (Lex (α × β))
Equations
instance Prod.Lex.inhabited (α : Type u_1) (β : Type u_2) [inst : Inhabited α] [inst : Inhabited β] :
Inhabited (Lex (α × β))
Equations
instance Prod.Lex.instLE (α : Type u_1) (β : Type u_2) [inst : LT α] [inst : LE β] :
LE (Lex (α × β))

Dictionary / lexicographic ordering on pairs.

Equations
instance Prod.Lex.instLT (α : Type u_1) (β : Type u_2) [inst : LT α] [inst : LT β] :
LT (Lex (α × β))
Equations
theorem Prod.Lex.le_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LE β] (a : α × β) (b : α × β) :
toLex a toLex b a.fst < b.fst a.fst = b.fst a.snd b.snd
theorem Prod.Lex.lt_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] (a : α × β) (b : α × β) :
toLex a < toLex b a.fst < b.fst a.fst = b.fst a.snd < b.snd
instance Prod.Lex.preorder (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst : Preorder β] :
Preorder (Lex (α × β))

Dictionary / lexicographic preorder for pairs.

Equations
  • One or more equations did not get rendered due to their size.
theorem Prod.Lex.toLex_mono {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] :
Monotone toLex
theorem Prod.Lex.toLex_strictMono {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] :
StrictMono toLex
instance Prod.Lex.partialOrder (α : Type u_1) (β : Type u_2) [inst : PartialOrder α] [inst : PartialOrder β] :
PartialOrder (Lex (α × β))

Dictionary / lexicographic partial order for pairs.

Equations
  • One or more equations did not get rendered due to their size.
instance Prod.Lex.linearOrder (α : Type u_1) (β : Type u_2) [inst : LinearOrder α] [inst : LinearOrder β] :
LinearOrder (Lex (α × β))

Dictionary / lexicographic linear order for pairs.

Equations
  • One or more equations did not get rendered due to their size.
instance Prod.Lex.orderBot {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] [inst : OrderBot α] [inst : OrderBot β] :
OrderBot (Lex (α × β))
Equations
instance Prod.Lex.orderTop {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] [inst : OrderTop α] [inst : OrderTop β] :
OrderTop (Lex (α × β))
Equations
instance Prod.Lex.boundedOrder {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] :
BoundedOrder (Lex (α × β))
Equations
  • Prod.Lex.boundedOrder = let src := Prod.Lex.orderBot; let src_1 := Prod.Lex.orderTop; BoundedOrder.mk