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

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

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

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

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

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

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

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

theorem Finsupp.Lex.single_lt_iff {α : Type u_1} [LinearOrder α] {a b : α} : toLex (single b 1) < toLex (single a 1) ↔ a < b

theorem Finsupp.Lex.single_le_iff {α : Type u_1} [LinearOrder α] {a b : α} : toLex (single b 1) ≤ toLex (single a 1) ↔ a ≤ b

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

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 b : Lex (α →₀ N)) (i : α) : (∀ j < i, (ofLex a) j = (ofLex b) j) → (ofLex a) i < (ofLex b) i → a < b

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

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.Lex.addLeftMono {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddLeftStrictMono N] : AddLeftMono (Lex (α →₀ N))

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

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

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

Equations

• Finsupp.Lex.orderBot = { bot := 0, bot_le := ⋯ }

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