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 α × β.

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 (· > ·) (· < ·).

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

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

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

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

theorem Pi.lex_iff_of_unique {ι : Type u_1} {β : ι → Type u_2} [Unique ι] [(i : ι) → LT (β i)] {r : ι → ι → Prop} [Std.Irrefl r] {x y : (i : ι) → β i} : Pi.Lex r (fun {i : ι} (x1 x2 : β i) => x1 < x2) x y ↔ x default < y default

theorem Pi.trichotomous_lex {ι : Type u_1} {β : ι → Type u_2} (r : ι → ι → Prop) (s : {i : ι} → β i → β i → Prop) [∀ (i : ι), Std.Trichotomous s] (wf : WellFounded r) : Std.Trichotomous (Pi.Lex r s)

@[deprecated Pi.trichotomous_lex (since := "2026-01-24")]

theorem Pi.isTrichotomous_lex {ι : Type u_1} {β : ι → Type u_2} (r : ι → ι → Prop) (s : {i : ι} → β i → β i → Prop) [∀ (i : ι), Std.Trichotomous s] (wf : WellFounded r) : Std.Trichotomous (Pi.Lex r s)

Alias of Pi.trichotomous_lex.

@[implicit_reducible]

instance Pi.instLTLexForall {ι : Type u_1} {β : ι → Type u_2} [LT ι] [(a : ι) → LT (β a)] : LT (Lex ((i : ι) → β i))

@[implicit_reducible]

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

@[simp]

theorem Pi.toLex_apply {ι : Type u_1} {β : ι → Type u_2} (x : (i : ι) → β i) (i : ι) : toLex x i = x i

@[simp]

theorem Pi.ofLex_apply {ι : Type u_1} {β : ι → Type u_2} (x : Lex ((i : ι) → β i)) (i : ι) : ofLex x i = x i

@[simp]

theorem Pi.toColex_apply {ι : Type u_1} {β : ι → Type u_2} (x : (i : ι) → β i) (i : ι) : toColex x i = x i

@[simp]

theorem Pi.ofColex_apply {ι : Type u_1} {β : ι → Type u_2} (x : Colex ((i : ι) → β i)) (i : ι) : ofColex x i = x i

theorem Pi.Lex.lt_iff_of_unique {ι : Type u_1} {β : ι → Type u_2} [Unique ι] [(i : ι) → LT (β i)] [Preorder ι] {x y : Lex ((i : ι) → β i)} : x < y ↔ x default < y default

@[deprecated Pi.Lex.lt_iff_of_unique (since := "2025-11-29")]

theorem Pi.lex_lt_iff_of_unique {ι : Type u_1} {β : ι → Type u_2} [Unique ι] [(i : ι) → LT (β i)] [Preorder ι] {x y : Lex ((i : ι) → β i)} : x < y ↔ x default < y default

Alias of Pi.Lex.lt_iff_of_unique.

theorem Pi.Colex.lt_iff_of_unique {ι : Type u_1} {β : ι → Type u_2} [Unique ι] [(i : ι) → LT (β i)] [Preorder ι] {x y : Colex ((i : ι) → β i)} : x < y ↔ x default < y default

@[deprecated Pi.Colex.lt_iff_of_unique (since := "2025-11-29")]

theorem Pi.colex_lt_iff_of_unique {ι : Type u_1} {β : ι → Type u_2} [Unique ι] [(i : ι) → LT (β i)] [Preorder ι] {x y : Colex ((i : ι) → β i)} : x < y ↔ x default < y default

Alias of Pi.Colex.lt_iff_of_unique.

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

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

@[implicit_reducible]

instance Pi.instPartialOrderLexForallOfLinearOrder {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [(a : ι) → PartialOrder (β a)] : PartialOrder (Lex ((i : ι) → β i))

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

theorem Pi.lex_le_iff_of_unique {ι : Type u_1} {β : ι → Type u_2} [Unique ι] [LinearOrder ι] [(i : ι) → PartialOrder (β i)] {x y : Lex ((i : ι) → β i)} : x ≤ y ↔ x default ≤ y default

theorem Pi.colex_le_iff_of_unique {ι : Type u_1} {β : ι → Type u_2} [Unique ι] [LinearOrder ι] [(i : ι) → PartialOrder (β i)] {x y : Colex ((i : ι) → β i)} : x ≤ y ↔ x default ≤ y default

theorem Pi.toLex_monotone {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [(i : ι) → PartialOrder (β i)] [WellFoundedLT ι] : Monotone ⇑toLex

theorem Pi.toLex_strictMono {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [(i : ι) → PartialOrder (β i)] [WellFoundedLT ι] : StrictMono ⇑toLex

@[simp]

theorem Pi.lt_toLex_update_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i} [(i : ι) → PartialOrder (β i)] [WellFoundedLT ι] : toLex x < toLex (Function.update x i a) ↔ x i < a

@[simp]

theorem Pi.toLex_update_lt_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i} [(i : ι) → PartialOrder (β i)] [WellFoundedLT ι] : toLex (Function.update x i a) < toLex x ↔ a < x i

@[simp]

theorem Pi.le_toLex_update_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i} [(i : ι) → PartialOrder (β i)] [WellFoundedLT ι] : toLex x ≤ toLex (Function.update x i a) ↔ x i ≤ a

@[simp]

theorem Pi.toLex_update_le_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i} [(i : ι) → PartialOrder (β i)] [WellFoundedLT ι] : toLex (Function.update x i a) ≤ toLex x ↔ a ≤ x i

theorem Pi.toColex_monotone {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [(i : ι) → PartialOrder (β i)] [WellFoundedGT ι] : Monotone ⇑toColex

theorem Pi.toColex_strictMono {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [(i : ι) → PartialOrder (β i)] [WellFoundedGT ι] : StrictMono ⇑toColex

@[simp]

theorem Pi.lt_toColex_update_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i} [(i : ι) → PartialOrder (β i)] [WellFoundedGT ι] : toColex x < toColex (Function.update x i a) ↔ x i < a

@[simp]

theorem Pi.toColex_update_lt_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i} [(i : ι) → PartialOrder (β i)] [WellFoundedGT ι] : toColex (Function.update x i a) < toColex x ↔ a < x i

@[simp]

theorem Pi.le_toColex_update_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i} [(i : ι) → PartialOrder (β i)] [WellFoundedGT ι] : toColex x ≤ toColex (Function.update x i a) ↔ x i ≤ a

@[simp]

theorem Pi.toColex_update_le_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i} [(i : ι) → PartialOrder (β i)] [WellFoundedGT ι] : toColex (Function.update x i a) ≤ toColex x ↔ a ≤ x i

theorem Pi.apply_le_of_toLex {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] {x y : (i : ι) → β i} {i : ι} [(i : ι) → LinearOrder (β i)] (hxy : toLex x ≤ toLex y) (h : ∀ j < i, x j = y j) : x i ≤ y i

theorem Pi.apply_le_of_toColex {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] {x y : (i : ι) → β i} {i : ι} [(i : ι) → LinearOrder (β i)] (hxy : toColex x ≤ toColex y) (h : ∀ j > i, x j = y j) : x i ≤ y i

@[implicit_reducible]

instance Pi.instOrderBotLexForallOfWellFoundedLT {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(a : ι) → PartialOrder (β a)] [(a : ι) → OrderBot (β a)] : OrderBot (Lex ((a : ι) → β a))

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

instance Pi.instDenselyOrderedLexForall {ι : Type u_1} {β : ι → Type u_2} [Preorder ι] [(i : ι) → LT (β i)] [∀ (i : ι), DenselyOrdered (β i)] : DenselyOrdered (Lex ((i : ι) → β i))

instance Pi.instDenselyOrderedColexForall {ι : Type u_1} {β : ι → Type u_2} [Preorder ι] [(i : ι) → LT (β i)] [∀ (i : ι), DenselyOrdered (β i)] : DenselyOrdered (Colex ((i : ι) → β i))

theorem Pi.Lex.noMaxOrder' {ι : Type u_1} {β : ι → Type u_2} [Preorder ι] [(i : ι) → LT (β i)] (i : ι) [NoMaxOrder (β i)] : NoMaxOrder (Lex ((i : ι) → β i))

theorem Pi.Colex.noMaxOrder' {ι : Type u_1} {β : ι → Type u_2} [Preorder ι] [(i : ι) → LT (β i)] (i : ι) [NoMaxOrder (β i)] : NoMaxOrder (Colex ((i : ι) → β i))

instance Pi.instNoMaxOrderLexForallOfWellFoundedLTOfNonempty {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [Nonempty ι] [(i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMaxOrder (β i)] : NoMaxOrder (Lex ((i : ι) → β i))

instance Pi.instNoMaxOrderColexForallOfWellFoundedGTOfNonempty {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [Nonempty ι] [(i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMaxOrder (β i)] : NoMaxOrder (Colex ((i : ι) → β i))

instance Pi.instNoMinOrderLexForallOfWellFoundedLTOfNonempty {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [Nonempty ι] [(i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMinOrder (β i)] : NoMinOrder (Lex ((i : ι) → β i))

instance Pi.instNoMinOrderColexForallOfWellFoundedGTOfNonempty {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [WellFoundedGT ι] [Nonempty ι] [(i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMinOrder (β i)] : NoMinOrder (Colex ((i : ι) → β i))

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.

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.