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

Equations

• Finsupp.Lex r s x y = Pi.Lex r (fun {i : α} => s) ⇑x ⇑y

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.instLTLex {α : Type u_1} {N : Type u_2} [Zero N] [LT α] [LT N] : LT (Lex (α →₀ N))

Equations

• Finsupp.instLTLex = { lt := fun (f g : Lex (α →₀ N)) => Finsupp.Lex (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : N) => x1 < x2) (ofLex f) (ofLex g) }

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 : α} (x1 x2 : N) => x1 < x2) ⇑x ⇑y

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

Equations

• ⋯ = ⋯

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.

Equations

• Finsupp.Lex.partialOrder = PartialOrder.mk ⋯

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.

Equations

• Finsupp.Lex.linearOrder = LinearOrder.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• Finsupp.Lex.orderBot = OrderBot.mk ⋯

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

Equations

• Finsupp.Lex.orderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

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

Equations

• Finsupp.Lex.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯

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

Equations

• Finsupp.Lex.linearOrderedCancelAddCommMonoid = LinearOrderedCancelAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

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

Equations

• Finsupp.Lex.linearOrderedAddCommGroup = LinearOrderedAddCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯