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
Instances For
    instance Prod.Lex.decidableEq (α : Type u_4) (β : Type u_5) [DecidableEq α] [DecidableEq β] :
    DecidableEq (Lex (α × β))
    Equations
    instance Prod.Lex.inhabited (α : Type u_4) (β : Type u_5) [Inhabited α] [Inhabited β] :
    Inhabited (Lex (α × β))
    Equations
    instance Prod.Lex.instLE (α : Type u_4) (β : Type u_5) [LT α] [LE β] :
    LE (Lex (α × β))

    Dictionary / lexicographic ordering on pairs.

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

    Dictionary / lexicographic preorder for pairs.

    Equations
    theorem Prod.Lex.monotone_fst {α : Type u_1} {β : Type u_2} [Preorder α] [LE β] (t : Lex (α × β)) (c : Lex (α × β)) (h : t c) :
    (ofLex t).1 (ofLex c).1
    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.

    Equations
    instance Prod.Lex.linearOrder (α : Type u_4) (β : Type u_5) [LinearOrder α] [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.instOrdLex {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
    Ord (Lex (α × β))
    Equations
    instance Prod.Lex.orderBot {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] :
    OrderBot (Lex (α × β))
    Equations
    instance Prod.Lex.orderTop {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] [OrderTop α] [OrderTop β] :
    OrderTop (Lex (α × β))
    Equations
    instance Prod.Lex.boundedOrder {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] :
    BoundedOrder (Lex (α × β))
    Equations
    • Prod.Lex.boundedOrder = let __src := Prod.Lex.orderBot; let __src_1 := Prod.Lex.orderTop; BoundedOrder.mk
    instance Prod.Lex.instDenselyOrderedLex {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] :
    Equations
    • =
    instance Prod.Lex.noMaxOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder α] :
    NoMaxOrder (Lex (α × β))
    Equations
    • =
    instance Prod.Lex.noMinOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder α] :
    NoMinOrder (Lex (α × β))
    Equations
    • =
    instance Prod.Lex.noMaxOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder β] :
    NoMaxOrder (Lex (α × β))
    Equations
    • =
    instance Prod.Lex.noMinOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder β] :
    NoMinOrder (Lex (α × β))
    Equations
    • =