Lexicographic order on finitely supported functions

This file defines the lexicographic order on Finsupp.

def Finsupp.Lex {α : Type u_1} {N : Type u_2} [Zero N] (r : α → α → Prop) (s : N → N → Prop) (x y : α →₀ N) : Prop

Finsupp.Lex r s is the lexicographic relation on α →₀ N, where α is ordered by r, and N is ordered by s.

The type synonym Lex (α →₀ N) has an order given by Finsupp.Lex (· < ·) (· < ·).

theorem Pi.lex_eq_finsupp_lex {α : Type u_1} {N : Type u_2} [Zero N] {r : α → α → Prop} {s : N → N → Prop} (a b : α →₀ N) : Pi.Lex r (fun {i : α} => s) ⇑a ⇑b = Finsupp.Lex r s a b

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

theorem Finsupp.lex_eq_invImage_dfinsupp_lex {α : Type u_1} {N : Type u_2} [Zero N] (r : α → α → Prop) (s : N → N → Prop) : Finsupp.Lex r s = InvImage (DFinsupp.Lex r fun (x : α) => s) toDFinsupp

@[implicit_reducible]

instance Finsupp.instLTLex {α : Type u_1} {N : Type u_2} [Zero N] [LT α] [LT N] : LT (Lex (α →₀ N))

@[implicit_reducible]

instance Finsupp.instLTColex {α : Type u_1} {N : Type u_2} [Zero N] [LT α] [LT N] : LT (Colex (α →₀ N))

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

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

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

Alias of Finsupp.Lex.lt_iff.

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

theorem Finsupp.lex_lt_of_lt_of_preorder {α : Type u_1} {N : Type u_2} [Zero N] [Preorder N] (r : α → α → Prop) [IsStrictOrder α r] {x y : α →₀ N} (hlt : x < y) : ∃ (i : α), (∀ (j : α), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

theorem Finsupp.lex_lt_of_lt {α : Type u_1} {N : Type u_2} [Zero N] [PartialOrder N] (r : α → α → Prop) [IsStrictOrder α r] {x y : α →₀ N} (hlt : x < y) : Pi.Lex r (fun {i : α} (x1 x2 : N) => x1 < x2) ⇑x ⇑y

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

theorem Finsupp.Lex.lt_iff_of_unique {α : Type u_1} {N : Type u_2} [Zero N] [Unique α] [LT N] [Preorder α] {x y : Lex (α →₀ N)} : x < y ↔ (ofLex x) default < (ofLex y) default

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

theorem Finsupp.lex_lt_iff_of_unique {α : Type u_1} {N : Type u_2} [Zero N] [Unique α] [LT N] [Preorder α] {x y : Lex (α →₀ N)} : x < y ↔ (ofLex x) default < (ofLex y) default

Alias of Finsupp.Lex.lt_iff_of_unique.

theorem Finsupp.Colex.lt_iff_of_unique {α : Type u_1} {N : Type u_2} [Zero N] [Unique α] [LT N] [Preorder α] {x y : Colex (α →₀ N)} : x < y ↔ (ofColex x) default < (ofColex y) default

instance Finsupp.Lex.isStrictOrder {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [PartialOrder N] : IsStrictOrder (Lex (α →₀ N)) fun (x1 x2 : Lex (α →₀ N)) => x1 < x2

instance Finsupp.Colex.isStrictOrder {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [PartialOrder N] : IsStrictOrder (Colex (α →₀ N)) fun (x1 x2 : Colex (α →₀ N)) => x1 < x2

@[implicit_reducible]

instance Finsupp.Lex.partialOrder {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [PartialOrder N] : PartialOrder (Lex (α →₀ N))

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

@[implicit_reducible]

instance Finsupp.Colex.partialOrder {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [PartialOrder N] : PartialOrder (Colex (α →₀ N))

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

@[implicit_reducible]

instance Finsupp.Lex.linearOrder {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [LinearOrder N] : LinearOrder (Lex (α →₀ N))

The linear order on Finsupps obtained by the lexicographic ordering.

@[implicit_reducible]

instance Finsupp.Colex.linearOrder {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [LinearOrder N] : LinearOrder (Colex (α →₀ N))

The linear order on Finsupps obtained by the colexicographic ordering.

theorem Finsupp.Lex.le_iff_of_unique {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [Unique α] [PartialOrder N] {x y : Lex (α →₀ N)} : x ≤ y ↔ (ofLex x) default ≤ (ofLex y) default

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

theorem Finsupp.lex_le_iff_of_unique {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [Unique α] [PartialOrder N] {x y : Lex (α →₀ N)} : x ≤ y ↔ (ofLex x) default ≤ (ofLex y) default

Alias of Finsupp.Lex.le_iff_of_unique.

theorem Finsupp.Colex.le_iff_of_unique {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [Unique α] [PartialOrder N] {x y : Colex (α →₀ N)} : x ≤ y ↔ (ofColex x) default ≤ (ofColex y) default

theorem Finsupp.Lex.single_strictAnti {α : Type u_1} [LinearOrder α] : StrictAnti fun (a : α) => toLex fun₀ | a => 1

theorem Finsupp.Colex.single_strictMono {α : Type u_1} [LinearOrder α] : StrictMono fun (a : α) => toColex fun₀ | a => 1

theorem Finsupp.Lex.single_lt_iff {α : Type u_1} [LinearOrder α] {a b : α} : ((toLex fun₀ | b => 1) < toLex fun₀ | a => 1) ↔ a < b

theorem Finsupp.Colex.single_lt_iff {α : Type u_1} [LinearOrder α] {a b : α} : ((toColex fun₀ | a => 1) < toColex fun₀ | b => 1) ↔ a < b

theorem Finsupp.Lex.single_le_iff {α : Type u_1} [LinearOrder α] {a b : α} : ((toLex fun₀ | b => 1) ≤ toLex fun₀ | a => 1) ↔ a ≤ b

theorem Finsupp.Colex.single_le_iff {α : Type u_1} [LinearOrder α] {a b : α} : ((toColex fun₀ | a => 1) ≤ toColex fun₀ | b => 1) ↔ a ≤ b

@[deprecated Finsupp.Lex.single_strictAnti (since := "2025-10-28")]

theorem Finsupp.Lex.single_antitone {α : Type u_1} [LinearOrder α] : Antitone fun (a : α) => toLex fun₀ | a => 1

theorem Finsupp.toLex_monotone {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [PartialOrder N] : Monotone ⇑toLex

theorem Finsupp.toColex_monotone {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [PartialOrder N] : Monotone ⇑toColex

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

theorem Finsupp.lt_of_forall_lt_of_lt {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [PartialOrder N] (a b : Lex (α →₀ N)) (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 (α →₀ N) may fail to be monotone, when it is "just" monotone on N.

See Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean for a counterexample.

instance Finsupp.Lex.addLeftStrictMono {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddLeftStrictMono N] : AddLeftStrictMono (Lex (α →₀ N))

instance Finsupp.Colex.addLeftStrictMono {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddLeftStrictMono N] : AddLeftStrictMono (Colex (α →₀ N))

instance Finsupp.Lex.addLeftMono {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddLeftStrictMono N] : AddLeftMono (Lex (α →₀ N))

instance Finsupp.Colex.addLeftMono {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddLeftStrictMono N] : AddLeftMono (Colex (α →₀ N))

instance Finsupp.Lex.addRightStrictMono {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddRightStrictMono N] : AddRightStrictMono (Lex (α →₀ N))

instance Finsupp.Colex.addRightStrictMono {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddRightStrictMono N] : AddRightStrictMono (Colex (α →₀ N))

instance Finsupp.Lex.addRightMono {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddRightStrictMono N] : AddRightMono (Lex (α →₀ N))

instance Finsupp.Colex.addRightMono {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddRightStrictMono N] : AddRightMono (Colex (α →₀ N))

@[implicit_reducible]

instance Finsupp.Lex.orderBot {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddCommMonoid N] [PartialOrder N] [CanonicallyOrderedAdd N] : OrderBot (Lex (α →₀ N))

@[implicit_reducible]

instance Finsupp.Colex.orderBot {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddCommMonoid N] [PartialOrder N] [CanonicallyOrderedAdd N] : OrderBot (Colex (α →₀ N))

instance Finsupp.Lex.isOrderedCancelAddMonoid {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddCommMonoid N] [PartialOrder N] [IsOrderedCancelAddMonoid N] : IsOrderedCancelAddMonoid (Lex (α →₀ N))

instance Finsupp.Colex.isOrderedCancelAddMonoid {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddCommMonoid N] [PartialOrder N] [IsOrderedCancelAddMonoid N] : IsOrderedCancelAddMonoid (Colex (α →₀ N))