# Lexicographic order on Pi types #

This file defines the lexicographic and colexicographic orders for Pi types.

- In the lexicographic order, `a` is less than `b` if `a i = b i` for all `i` up to some point `k`, and `a k < b k`.
- In the colexicographic order, `a` is less than `b` if `a i = b i` for all `i` above some point `k`, and `a k < b k`.

## Notation #

- `Πₗ i, α i`: Pi type equipped with the lexicographic order. Type synonym of `Π i, α i`.

## See also #

Related files are:

- `Data.Finset.Colex`: Colexicographic order on finite sets.
- `Data.List.Lex`: Lexicographic order on lists.
- `Data.Sigma.Order`: Lexicographic order on `Σₗ i, α i`.
- `Data.PSigma.Order`: Lexicographic order on `Σₗ' i, α i`.
- `Data.Prod.Lex`: Lexicographic order on `α × β`.

source
def Pi.Lex {ι : Type u_1} {β : ι → Type u_2} (r : ι → ι → Prop) (s : {i : ι} → β i → β i → Prop) (x y : (i : ι) → β i) :
Prop

The lexicographic relation on `Π i : ι, β i`, where `ι` is ordered by `r`, and each `β i` is ordered by `s`.

The `<` relation on `Lex (∀ i, β i)` is `Pi.Lex (· < ·) (· < ·)`, while the `<` relation on `Colex (∀ i, β i)` is `Pi.Lex (· > ·) (· < ·)`.

Equations

- Pi.Lex r s x y = ∃ (i : ι), (∀ (j : ι), r j i → x j = y j) ∧ s (x i) (y i)

Instances For

source
def Pi.«termΠₗ_,_» :
Lean.ParserDescr

The notation `Πₗ i, α i` refers to a pi type equipped with the lexicographic order.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Pi.lex_lt_of_lt_of_preorder {ι : Type u_1} {β : ι → Type u_2} [(i : ι) → Preorder (β i)] {r : ι → ι → Prop} (hwf : WellFounded r) {x y : (i : ι) → β i} (hlt : x < y) :
∃ (i : ι), (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
source
theorem Pi.lex_lt_of_lt {ι : Type u_1} {β : ι → Type u_2} [(i : ι) → PartialOrder (β i)] {r : ι → ι → Prop} (hwf : WellFounded r) {x y : (i : ι) → β i} (hlt : x < y) :
Pi.Lex r (fun {i : ι} (x1 x2 : β i) => x1 < x2) x y
source
theorem Pi.isTrichotomous_lex {ι : Type u_1} {β : ι → Type u_2} (r : ι → ι → Prop) (s : {i : ι} → β i → β i → Prop) [∀ (i : ι), IsTrichotomous (β i) s] (wf : WellFounded r) :
IsTrichotomous ((i : ι) → β i) (Pi.Lex r s)
source
instance Pi.instLTLexForall {ι : Type u_1} {β : ι → Type u_2} [LT ι] [(a : ι) → LT (β a)] :
LT (Lex ((i : ι) → β i))
Equations

- Pi.instLTLexForall = { lt := Pi.Lex (fun (x1 x2 : ι) => x1 < x2) fun {i : ι} (x1 x2 : β i) => x1 < x2 }

source
instance Pi.instLTColexForall {ι : Type u_1} {β : ι → Type u_2} [LT ι] [(a : ι) → LT (β a)] :
LT (Colex ((i : ι) → β i))
Equations

- Pi.instLTColexForall = { lt := Pi.Lex (fun (x1 x2 : ι) => x1 > x2) fun {i : ι} (x1 x2 : β i) => x1 < x2 }

source
@[simp]
theorem Pi.toLex_apply {ι : Type u_1} {β : ι → Type u_2} (x : (i : ι) → β i) (i : ι) :
toLex x i = x i
source
@[simp]
theorem Pi.ofLex_apply {ι : Type u_1} {β : ι → Type u_2} (x : Lex ((i : ι) → β i)) (i : ι) :
ofLex x i = x i
source
@[simp]
theorem Pi.toColex_apply {ι : Type u_1} {β : ι → Type u_2} (x : (i : ι) → β i) (i : ι) :
toColex x i = x i
source
@[simp]
theorem Pi.ofColex_apply {ι : Type u_1} {β : ι → Type u_2} (x : Colex ((i : ι) → β i)) (i : ι) :
ofColex x i = x i
source
instance Pi.Lex.isStrictOrder {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [(a : ι) → PartialOrder (β a)] :
IsStrictOrder (Lex ((i : ι) → β i)) fun (x1 x2 : Lex ((i : ι) → β i)) => x1 < x2
source
instance Pi.Colex.isStrictOrder {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [(a : ι) → PartialOrder (β a)] :
IsStrictOrder (Colex ((i : ι) → β i)) fun (x1 x2 : Colex ((i : ι) → β i)) => x1 < x2
source
instance Pi.instPartialOrderLexForallOfLinearOrder {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [(a : ι) → PartialOrder (β a)] :
PartialOrder (Lex ((i : ι) → β i))
Equations

- Pi.instPartialOrderLexForallOfLinearOrder = partialOrderOfSO fun (x1 x2 : Lex ((i : ι) → β i)) => x1 < x2

source
instance Pi.instPartialOrderColexForallOfLinearOrder {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [(a : ι) → PartialOrder (β a)] :
PartialOrder (Colex ((i : ι) → β i))
Equations

- Pi.instPartialOrderColexForallOfLinearOrder = partialOrderOfSO fun (x1 x2 : Colex ((i : ι) → β i)) => x1 < x2

source
noncomputable instance Pi.Lex.linearOrder {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(a : ι) → LinearOrder (β a)] :
LinearOrder (Lex ((i : ι) → β i))

`Lex (∀ i, α i)` is a linear order if the original order has well-founded `<`.

Equations

- Pi.Lex.linearOrder = linearOrderOfSTO fun (x1 x2 : Lex ((i : ι) → (fun (i : ι) => β i) i)) => x1 < x2

source
noncomputable instance Pi.Colex.linearOrder {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [(a : ι) → LinearOrder (β a)] :
LinearOrder (Colex ((i : ι) → β i))

`Colex (∀ i, α i)` is a linear order if the original order has well-founded `>`.

Equations

- Pi.Colex.linearOrder = Pi.Lex.linearOrder

source
theorem Pi.toLex_monotone {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(i : ι) → PartialOrder (β i)] :
Monotone ⇑toLex
source
theorem Pi.toLex_strictMono {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(i : ι) → PartialOrder (β i)] :
StrictMono ⇑toLex
source
@[simp]
theorem Pi.lt_toLex_update_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} :
toLex x < toLex (Function.update x i a) ↔ x i < a
source
@[simp]
theorem Pi.toLex_update_lt_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} :
toLex (Function.update x i a) < toLex x ↔ a < x i
source
@[simp]
theorem Pi.le_toLex_update_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} :
toLex x ≤ toLex (Function.update x i a) ↔ x i ≤ a
source
@[simp]
theorem Pi.toLex_update_le_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} :
toLex (Function.update x i a) ≤ toLex x ↔ a ≤ x i
source
theorem Pi.toColex_monotone {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [(i : ι) → PartialOrder (β i)] :
Monotone ⇑toColex
source
theorem Pi.toColex_strictMono {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [(i : ι) → PartialOrder (β i)] :
StrictMono ⇑toColex
source
@[simp]
theorem Pi.lt_toColex_update_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} :
toColex x < toColex (Function.update x i a) ↔ x i < a
source
@[simp]
theorem Pi.toColex_update_lt_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} :
toColex (Function.update x i a) < toColex x ↔ a < x i
source
@[simp]
theorem Pi.le_toColex_update_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} :
toColex x ≤ toColex (Function.update x i a) ↔ x i ≤ a
source
@[simp]
theorem Pi.toColex_update_le_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} :
toColex (Function.update x i a) ≤ toColex x ↔ a ≤ x i
source
instance Pi.instOrderBotLexForallOfWellFoundedLT {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(a : ι) → PartialOrder (β a)] [(a : ι) → OrderBot (β a)] :
OrderBot (Lex ((a : ι) → β a))
Equations

- Pi.instOrderBotLexForallOfWellFoundedLT = { bot := toLex ⊥, bot_le := ⋯ }

source
instance Pi.instOrderBotColexForallOfWellFoundedGT {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [(a : ι) → PartialOrder (β a)] [(a : ι) → OrderBot (β a)] :
OrderBot (Colex ((a : ι) → β a))
Equations

- Pi.instOrderBotColexForallOfWellFoundedGT = { bot := toColex ⊥, bot_le := ⋯ }

source
instance Pi.instOrderTopLexForallOfWellFoundedLT {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(a : ι) → PartialOrder (β a)] [(a : ι) → OrderTop (β a)] :
OrderTop (Lex ((a : ι) → β a))
Equations

- Pi.instOrderTopLexForallOfWellFoundedLT = { top := toLex ⊤, le_top := ⋯ }

source
instance Pi.instOrderTopColexForallOfWellFoundedGT {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [(a : ι) → PartialOrder (β a)] [(a : ι) → OrderTop (β a)] :
OrderTop (Colex ((a : ι) → β a))
Equations

- Pi.instOrderTopColexForallOfWellFoundedGT = { top := toColex ⊤, le_top := ⋯ }

source
instance Pi.instBoundedOrderLexForallOfWellFoundedLT {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(a : ι) → PartialOrder (β a)] [(a : ι) → BoundedOrder (β a)] :
BoundedOrder (Lex ((a : ι) → β a))
Equations

- Pi.instBoundedOrderLexForallOfWellFoundedLT = { toOrderTop := Pi.instOrderTopLexForallOfWellFoundedLT, toOrderBot := Pi.instOrderBotLexForallOfWellFoundedLT }

source
instance Pi.instBoundedOrderColexForallOfWellFoundedGT {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [(a : ι) → PartialOrder (β a)] [(a : ι) → BoundedOrder (β a)] :
BoundedOrder (Colex ((a : ι) → β a))
Equations

- Pi.instBoundedOrderColexForallOfWellFoundedGT = { toOrderTop := Pi.instOrderTopColexForallOfWellFoundedGT, toOrderBot := Pi.instOrderBotColexForallOfWellFoundedGT }

source
instance Pi.instDenselyOrderedLexForall {ι : Type u_1} {β : ι → Type u_2} [Preorder ι] [(i : ι) → LT (β i)] [∀ (i : ι), DenselyOrdered (β i)] :
DenselyOrdered (Lex ((i : ι) → β i))
source
instance Pi.instDenselyOrderedColexForall {ι : Type u_1} {β : ι → Type u_2} [Preorder ι] [(i : ι) → LT (β i)] [∀ (i : ι), DenselyOrdered (β i)] :
DenselyOrdered (Colex ((i : ι) → β i))
source
theorem Pi.Lex.noMaxOrder' {ι : Type u_1} {β : ι → Type u_2} [Preorder ι] [(i : ι) → LT (β i)] (i : ι) [NoMaxOrder (β i)] :
NoMaxOrder (Lex ((i : ι) → β i))
source
theorem Pi.Colex.noMaxOrder' {ι : Type u_1} {β : ι → Type u_2} [Preorder ι] [(i : ι) → LT (β i)] (i : ι) [NoMaxOrder (β i)] :
NoMaxOrder (Colex ((i : ι) → β i))
source
instance Pi.instNoMaxOrderLexForallOfWellFoundedLTOfNonempty {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [Nonempty ι] [(i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMaxOrder (β i)] :
NoMaxOrder (Lex ((i : ι) → β i))
source
instance Pi.instNoMaxOrderColexForallOfWellFoundedGTOfNonempty {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [Nonempty ι] [(i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMaxOrder (β i)] :
NoMaxOrder (Colex ((i : ι) → β i))
source
instance Pi.instNoMinOrderLexForallOfWellFoundedLTOfNonempty {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [Nonempty ι] [(i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMinOrder (β i)] :
NoMinOrder (Lex ((i : ι) → β i))
source
instance Pi.instNoMinOrderColexForallOfWellFoundedGTOfNonempty {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [Nonempty ι] [(i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMinOrder (β i)] :
NoMinOrder (Colex ((i : ι) → β i))
source
theorem Pi.lex_desc {ι : Type u_1} {α : Type u_3} [Preorder ι] [DecidableEq ι] [LT α] {f : ι → α} {i j : ι} (h₁ : i ≤ j) (h₂ : f j < f i) :
toLex (f ∘ ⇑(Equiv.swap i j)) < toLex f

If we swap two strictly decreasing values in a function, then the result is lexicographically smaller than the original function.

source
theorem Pi.colex_asc {ι : Type u_1} {α : Type u_3} [Preorder ι] [DecidableEq ι] [LT α] {f : ι → α} {i j : ι} (h₁ : i ≤ j) (h₂ : f i < f j) :
toColex (f ∘ ⇑(Equiv.swap i j)) < toColex f

If we swap two strictly increasing values in a function, then the result is colexicographically smaller than the original function.