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.instLE (α : Type u_3) (β : Type u_4) [LT α] [LE β] :
      LE (Lex (α × β))

      Dictionary / lexicographic ordering on pairs.

      Equations
        instance Prod.Lex.instLT (α : Type u_3) (β : Type u_4) [LT α] [LT β] :
        LT (Lex (α × β))
        Equations
          theorem Prod.Lex.toLex_le_toLex {α : Type u_1} {β : Type u_2} [LT α] [LE β] {x y : α × β} :
          toLex x toLex y x.1 < y.1 x.1 = y.1 x.2 y.2
          theorem Prod.Lex.toLex_lt_toLex {α : Type u_1} {β : Type u_2} [LT α] [LT β] {x y : α × β} :
          toLex x < toLex y x.1 < y.1 x.1 = y.1 x.2 < y.2
          theorem Prod.Lex.le_iff {α : Type u_1} {β : Type u_2} [LT α] [LE β] {x y : Lex (α × β)} :
          x y (ofLex x).1 < (ofLex y).1 (ofLex x).1 = (ofLex y).1 (ofLex x).2 (ofLex y).2
          theorem Prod.Lex.lt_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {x y : Lex (α × β)} :
          x < y (ofLex x).1 < (ofLex y).1 (ofLex x).1 = (ofLex y).1 (ofLex x).2 < (ofLex y).2
          instance Prod.Lex.instWellFoundedLTLex {α : Type u_1} {β : Type u_2} [LT α] [LT β] [WellFoundedLT α] [WellFoundedLT β] :
          WellFoundedLT (Lex (α × β))
          Equations
            instance Prod.Lex.instPreorder (α : Type u_3) (β : Type u_4) [Preorder α] [Preorder β] :
            Preorder (Lex (α × β))

            Dictionary / lexicographic preorder for pairs.

            Equations
              theorem Prod.Lex.monotone_fst {α : Type u_1} {β : Type u_2} [Preorder α] [LE β] (t c : Lex (α × β)) (h : t c) :
              (ofLex t).1 (ofLex c).1

              See also monotone_fst_ofLex for a version stated in terms of Monotone.

              theorem Prod.Lex.monotone_fst_ofLex {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
              Monotone fun (x : Lex (α × β)) => (ofLex x).1
              theorem Prod.Lex.toLex_covBy_toLex_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a₁ a₂ : α} {b₁ b₂ : β} :
              toLex (a₁, b₁) toLex (a₂, b₂) a₁ = a₂ b₁ b₂ a₁ a₂ IsMax b₁ IsMin b₂
              theorem Prod.Lex.covBy_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : Lex (α × β)} :
              a b (ofLex a).1 = (ofLex b).1 (ofLex a).2 (ofLex b).2 (ofLex a).1 (ofLex b).1 IsMax (ofLex a).2 IsMin (ofLex b).2
              theorem Prod.Lex.toLex_le_toLex' {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {x y : α × β} :
              toLex x toLex y x.1 y.1 (x.1 = y.1x.2 y.2)

              Variant of Prod.Lex.toLex_le_toLex for partial orders.

              theorem Prod.Lex.toLex_lt_toLex' {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {x y : α × β} :
              toLex x < toLex y x.1 y.1 (x.1 = y.1x.2 < y.2)

              Variant of Prod.Lex.toLex_lt_toLex for partial orders.

              theorem Prod.Lex.le_iff' {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {x y : Lex (α × β)} :
              x y (ofLex x).1 (ofLex y).1 ((ofLex x).1 = (ofLex y).1(ofLex x).2 (ofLex y).2)

              Variant of Prod.Lex.le_iff for partial orders.

              theorem Prod.Lex.lt_iff' {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {x y : Lex (α × β)} :
              x < y (ofLex x).1 (ofLex y).1 ((ofLex x).1 = (ofLex y).1(ofLex x).2 < (ofLex y).2)

              Variant of Prod.Lex.lt_iff for partial orders.

              theorem Prod.Lex.toLex_mono {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] :
              theorem Prod.Lex.toLex_strictMono {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] :
              instance Prod.Lex.instPartialOrder (α : Type u_3) (β : Type u_4) [PartialOrder α] [PartialOrder β] :
              PartialOrder (Lex (α × β))

              Dictionary / lexicographic partial order for pairs.

              Equations
                instance Prod.Lex.instOrdLexProd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
                Ord (Lex (α × β))
                Equations
                  theorem Prod.Lex.compare_def {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
                  compare = compareLex (compareOn fun (x : Lex (α × β)) => (ofLex x).1) (compareOn fun (x : Lex (α × β)) => (ofLex x).2)
                  theorem lexOrd_eq {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
                  theorem Ord.lex_eq {α : Type u_1} {β : Type u_2} [ : Ord α] [ : Ord β] :
                  instance Prod.Lex.instTransOrdLex {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [Batteries.TransOrd α] [Batteries.TransOrd β] :
                  instance Prod.Lex.instLinearOrder (α : Type u_3) (β : Type u_4) [LinearOrder α] [LinearOrder β] :
                  LinearOrder (Lex (α × β))

                  Dictionary / lexicographic linear order for pairs.

                  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
                          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 (α × β))