Lexicographic order on finitely supported dependent functions

This file defines the lexicographic order on DFinsupp.

def DFinsupp.Lex {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] (r : ι → ι → Prop) (s : (i : ι) → α i → α i → Prop) (x y : Π₀ (i : ι), α i) : Prop

DFinsupp.Lex r s is the lexicographic relation on Π₀ i, α i, where ι is ordered by r, and α i is ordered by s i.

The type synonym Lex (Π₀ i, α i) has an order given by DFinsupp.Lex (· < ·) (· < ·), whereas Colex (Π₀ i, α i) has an order given by DFinsupp.Lex (· > ·) (· < ·).

theorem Pi.lex_eq_dfinsupp_lex {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} (a b : Π₀ (i : ι), α i) : Pi.Lex r (fun {i : ι} => s i) ⇑a ⇑b = DFinsupp.Lex r s a b

theorem DFinsupp.lex_def {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {a b : Π₀ (i : ι), α i} : DFinsupp.Lex r s a b ↔ ∃ (j : ι), (∀ (d : ι), r d j → a d = b d) ∧ s j (a j) (b j)

@[implicit_reducible]

instance DFinsupp.instLTLex {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LT ι] [(i : ι) → LT (α i)] : LT (Lex (Π₀ (i : ι), α i))

@[implicit_reducible]

instance DFinsupp.instLTColex {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LT ι] [(i : ι) → LT (α i)] : LT (Colex (Π₀ (i : ι), α i))

theorem DFinsupp.Lex.lt_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LT ι] [(i : ι) → LT (α i)] {a b : Lex (Π₀ (i : ι), α i)} : a < b ↔ ∃ (i : ι), (∀ j < i, (ofLex a) j = (ofLex b) j) ∧ (ofLex a) i < (ofLex b) i

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

theorem DFinsupp.lex_lt_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LT ι] [(i : ι) → LT (α i)] {a b : Lex (Π₀ (i : ι), α i)} : a < b ↔ ∃ (i : ι), (∀ j < i, (ofLex a) j = (ofLex b) j) ∧ (ofLex a) i < (ofLex b) i

Alias of DFinsupp.Lex.lt_iff.

theorem DFinsupp.Colex.lt_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LT ι] [(i : ι) → LT (α i)] {a b : Colex (Π₀ (i : ι), α i)} : a < b ↔ ∃ (i : ι), (∀ (j : ι), i < j → (ofColex a) j = (ofColex b) j) ∧ (ofColex a) i < (ofColex b) i

theorem DFinsupp.lex_lt_of_lt_of_preorder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] (r : ι → ι → Prop) [IsStrictOrder ι 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 DFinsupp.lex_lt_of_lt {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] (r : ι → ι → Prop) [IsStrictOrder ι r] {x y : Π₀ (i : ι), α i} (hlt : x < y) : Pi.Lex r (fun {i : ι} (x1 x2 : α i) => x1 < x2) ⇑x ⇑y

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

theorem DFinsupp.Lex.lt_iff_of_unique {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [Unique ι] [(i : ι) → LT (α i)] [Preorder ι] {x y : Lex (Π₀ (i : ι), α i)} : x < y ↔ (ofLex x) default < (ofLex y) default

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

theorem DFinsupp.lex_lt_iff_of_unique {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [Unique ι] [(i : ι) → LT (α i)] [Preorder ι] {x y : Lex (Π₀ (i : ι), α i)} : x < y ↔ (ofLex x) default < (ofLex y) default

Alias of DFinsupp.Lex.lt_iff_of_unique.

theorem DFinsupp.colex_lt_iff_of_unique {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [Unique ι] [(i : ι) → LT (α i)] [Preorder ι] {x y : Colex (Π₀ (i : ι), α i)} : x < y ↔ (ofColex x) default < (ofColex y) default

instance DFinsupp.Lex.isStrictOrder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → PartialOrder (α i)] : IsStrictOrder (Lex (Π₀ (i : ι), α i)) fun (x1 x2 : Lex (Π₀ (i : ι), α i)) => x1 < x2

instance DFinsupp.Colex.isStrictOrder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → PartialOrder (α i)] : IsStrictOrder (Colex (Π₀ (i : ι), α i)) fun (x1 x2 : Colex (Π₀ (i : ι), α i)) => x1 < x2

@[implicit_reducible]

instance DFinsupp.Lex.partialOrder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → PartialOrder (α i)] : PartialOrder (Lex (Π₀ (i : ι), α i))

The partial order on DFinsupps obtained by the lexicographic ordering. See DFinsupp.Lex.linearOrder for a proof that this partial order is in fact linear.

@[implicit_reducible]

instance DFinsupp.Colex.partialOrder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → PartialOrder (α i)] : PartialOrder (Colex (Π₀ (i : ι), α i))

The partial order on DFinsupps obtained by the colexicographic ordering. See DFinsupp.Colex.linearOrder for a proof that this partial order is in fact linear.

theorem DFinsupp.Lex.le_iff_of_unique {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [Unique ι] [(i : ι) → PartialOrder (α i)] {x y : Lex (Π₀ (i : ι), α i)} : x ≤ y ↔ (ofLex x) default ≤ (ofLex y) default

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

theorem DFinsupp.lex_le_iff_of_unique {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [Unique ι] [(i : ι) → PartialOrder (α i)] {x y : Lex (Π₀ (i : ι), α i)} : x ≤ y ↔ (ofLex x) default ≤ (ofLex y) default

Alias of DFinsupp.Lex.le_iff_of_unique.

theorem DFinsupp.Colex.le_iff_of_unique {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [Unique ι] [(i : ι) → PartialOrder (α i)] {x y : Colex (Π₀ (i : ι), α i)} : x ≤ y ↔ (ofColex x) default ≤ (ofColex y) default

instance DFinsupp.Lex.total_le {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : Std.Total fun (x1 x2 : Lex (Π₀ (i : ι), α i)) => x1 ≤ x2

instance DFinsupp.Colex.total_le {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : Std.Total fun (x1 x2 : Colex (Π₀ (i : ι), α i)) => x1 ≤ x2

@[implicit_reducible]

instance DFinsupp.Lex.decidableLE {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : DecidableLE (Lex (Π₀ (i : ι), α i))

The less-or-equal relation for the lexicographic ordering is decidable.

@[implicit_reducible]

instance DFinsupp.Colex.decidableLE {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : DecidableLE (Colex (Π₀ (i : ι), α i))

The less-or-equal relation for the colexicographic ordering is decidable.

@[implicit_reducible]

instance DFinsupp.Lex.decidableLT {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : DecidableLT (Lex (Π₀ (i : ι), α i))

The less-than relation for the lexicographic ordering is decidable.

@[implicit_reducible]

instance DFinsupp.Colex.decidableLT {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : DecidableLT (Colex (Π₀ (i : ι), α i))

The less-than relation for the colexicographic ordering is decidable.

@[implicit_reducible]

instance DFinsupp.Lex.linearOrder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : LinearOrder (Lex (Π₀ (i : ι), α i))

The linear order on DFinsupps obtained by the lexicographic ordering.

@[implicit_reducible]

instance DFinsupp.Colex.linearOrder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : LinearOrder (Colex (Π₀ (i : ι), α i))

The linear order on DFinsupps obtained by the colexicographic ordering.

theorem DFinsupp.toLex_monotone {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → PartialOrder (α i)] : Monotone ⇑toLex

theorem DFinsupp.toColex_monotone {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → PartialOrder (α i)] : Monotone ⇑toColex

@[deprecated DFinsupp.Lex.lt_iff (since := "2025-10-12")]

theorem DFinsupp.lt_of_forall_lt_of_lt {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → PartialOrder (α i)] (a b : Lex (Π₀ (i : ι), α i)) (i : ι) : (∀ j < i, (ofLex a) j = (ofLex b) j) → (ofLex a) i < (ofLex b) i → a < b

We are about to sneak in a hypothesis that might appear to be too strong. We assume AddLeftStrictMono (covariant with strict inequality <) also when proving the one with the weak inequality ≤. This is actually necessary: addition on Lex (Π₀ i, α i) may fail to be monotone, when it is "just" monotone on α i.

instance DFinsupp.Lex.addLeftStrictMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)] : AddLeftStrictMono (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Colex.addLeftStrictMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)] : AddLeftStrictMono (Colex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.addLeftMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)] : AddLeftMono (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Colex.addLeftMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)] : AddLeftMono (Colex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.addRightStrictMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)] : AddRightStrictMono (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Colex.addRightStrictMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)] : AddRightStrictMono (Colex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.addRightMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)] : AddRightMono (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Colex.addRightMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)] : AddRightMono (Colex (Π₀ (i : ι), α i))

@[implicit_reducible]

instance DFinsupp.Lex.orderBot {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] : OrderBot (Lex (Π₀ (i : ι), α i))

@[implicit_reducible]

instance DFinsupp.Colex.orderBot {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] : OrderBot (Colex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.isOrderedCancelAddMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedCancelAddMonoid (α i)] : IsOrderedCancelAddMonoid (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Colex.isOrderedCancelAddMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedCancelAddMonoid (α i)] : IsOrderedCancelAddMonoid (Colex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.isOrderedAddMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddCommGroup (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedAddMonoid (α i)] : IsOrderedAddMonoid (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Colex.isOrderedAddMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddCommGroup (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedAddMonoid (α i)] : IsOrderedAddMonoid (Colex (Π₀ (i : ι), α i))