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 : α →₀ N) (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 : α →₀ N) (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 : α →₀ N} {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) Finsupp.toDFinsupp

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

theorem Finsupp.lex_lt_of_lt_of_preorder {α : Type u_1} {N : Type u_2} [Zero N] [Preorder N] (r : α → α → Prop) [IsStrictOrder α r] {x : α →₀ N} {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 : α →₀ N} {y : α →₀ N} (hlt : x < y) : Pi.Lex r (fun {i} x x_1 => x < x_1) ↑x ↑y

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

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.

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.

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

theorem Finsupp.lt_of_forall_lt_of_lt {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [PartialOrder N] (a : Lex (α →₀ N)) (b : Lex (α →₀ N)) (i : α) : (∀ (j : α), 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 CovariantClass 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.covariantClass_lt_left {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1] : CovariantClass (Lex (α →₀ N)) (Lex (α →₀ N)) (fun x x_1 => x + x_1) fun x x_1 => x < x_1

instance Finsupp.Lex.covariantClass_le_left {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1] : CovariantClass (Lex (α →₀ N)) (Lex (α →₀ N)) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

instance Finsupp.Lex.covariantClass_lt_right {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] : CovariantClass (Lex (α →₀ N)) (Lex (α →₀ N)) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1

instance Finsupp.Lex.covariantClass_le_right {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] : CovariantClass (Lex (α →₀ N)) (Lex (α →₀ N)) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

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

noncomputable instance Finsupp.Lex.orderedAddCancelCommMonoid {α : Type u_1} {N : Type u_2} [LinearOrder α] [OrderedCancelAddCommMonoid N] : OrderedCancelAddCommMonoid (Lex (α →₀ N))

noncomputable instance Finsupp.Lex.orderedAddCommGroup {α : Type u_1} {N : Type u_2} [LinearOrder α] [OrderedAddCommGroup N] : OrderedAddCommGroup (Lex (α →₀ N))

noncomputable instance Finsupp.Lex.linearOrderedCancelAddCommMonoid {α : Type u_1} {N : Type u_2} [LinearOrder α] [LinearOrderedCancelAddCommMonoid N] : LinearOrderedCancelAddCommMonoid (Lex (α →₀ N))

noncomputable instance Finsupp.Lex.linearOrderedAddCommGroup {α : Type u_1} {N : Type u_2} [LinearOrder α] [LinearOrderedAddCommGroup N] : LinearOrderedAddCommGroup (Lex (α →₀ N))