Documentation

Mathlib.Data.Finsupp.Lex

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 : NNProp) (x y : α →₀ N) :

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
theorem Pi.lex_eq_finsupp_lex {α : Type u_1} {N : Type u_2} [Zero N] {r : ααProp} {s : NNProp} (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 : NNProp} {a b : α →₀ N} :
Finsupp.Lex r s a b ∃ (j : α), (∀ (d : α), r d ja 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 : NNProp) :
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
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 ix 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] :

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
instance Finsupp.Lex.linearOrder {α : Type u_1} {N : Type u_2} [Zero N] [LinearOrder α] [LinearOrder N] :

The linear order on Finsupps obtained by the lexicographic ordering.

Equations
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] :
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) ia < 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.