Lexicographic order #
This file defines the lexicographic relation for pairs of orders, partial orders and linear orders.
Main declarations #
Prod.Lex.
: Instances lifting the orders onOrder
α
andβ
toα ×ₗ β
.
Notation #
α ×ₗ β
:α × β
equipped with the lexicographic order
See also #
Related files are:
A type synonym to equip a type with its lexicographic order.
Instances For
instance
Prod.Lex.decidableEq
(α : Type u_4)
(β : Type u_5)
[DecidableEq α]
[DecidableEq β]
:
DecidableEq (Lex (α × β))
theorem
Prod.Lex.toLex_mono
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[Preorder β]
:
Monotone ↑toLex
theorem
Prod.Lex.toLex_strictMono
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[Preorder β]
:
StrictMono ↑toLex
instance
Prod.Lex.partialOrder
(α : Type u_4)
(β : Type u_5)
[PartialOrder α]
[PartialOrder β]
:
PartialOrder (Lex (α × β))
Dictionary / lexicographic partial order for pairs.
instance
Prod.Lex.linearOrder
(α : Type u_4)
(β : Type u_5)
[LinearOrder α]
[LinearOrder β]
:
LinearOrder (Lex (α × β))
Dictionary / lexicographic linear order for pairs.
instance
Prod.Lex.boundedOrder
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[Preorder β]
[BoundedOrder α]
[BoundedOrder β]
:
BoundedOrder (Lex (α × β))
instance
Prod.Lex.instDenselyOrderedLexProdInstLTToLTToLT
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[DenselyOrdered α]
[DenselyOrdered β]
:
DenselyOrdered (Lex (α × β))
instance
Prod.Lex.noMaxOrder_of_left
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[NoMaxOrder α]
:
NoMaxOrder (Lex (α × β))
instance
Prod.Lex.noMinOrder_of_left
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[NoMinOrder α]
:
NoMinOrder (Lex (α × β))
instance
Prod.Lex.noMaxOrder_of_right
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[NoMaxOrder β]
:
NoMaxOrder (Lex (α × β))
instance
Prod.Lex.noMinOrder_of_right
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[NoMinOrder β]
:
NoMinOrder (Lex (α × β))