mathlib documentation

data.finsupp.lex

Lexicographic order on finitely supported functions #

This file defines the lexicographic order on finsupp.

@[protected]
def finsupp.lex {α : Type u_1} {N : Type u_2} [has_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
theorem pi.lex_eq_finsupp_lex {α : Type u_1} {N : Type u_2} [has_zero N] {r : α α Prop} {s : N N Prop} (a b : α →₀ N) :
pi.lex r (λ (_x : α), s) a b = finsupp.lex r s a b
theorem finsupp.lex_def {α : Type u_1} {N : Type u_2} [has_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_inv_image_dfinsupp_lex {α : Type u_1} {N : Type u_2} [has_zero N] (r : α α Prop) (s : N N Prop) :
@[protected, instance]
def finsupp.lex.has_lt {α : Type u_1} {N : Type u_2} [has_zero N] [has_lt α] [has_lt N] :
has_lt (lex →₀ N))
Equations
theorem finsupp.lex_lt_of_lt_of_preorder {α : Type u_1} {N : Type u_2} [has_zero N] [preorder N] (r : α α Prop) [is_strict_order α 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} [has_zero N] [partial_order N] (r : α α Prop) [is_strict_order α r] {x y : α →₀ N} (hlt : x < y) :
pi.lex r (λ (i : α), has_lt.lt) x y
@[protected, instance]
@[protected, instance]
def finsupp.lex.partial_order {α : Type u_1} {N : Type u_2} [has_zero N] [linear_order α] [partial_order N] :

The partial order on finsupps obtained by the lexicographic ordering. See finsupp.lex.linear_order for a proof that this partial order is in fact linear.

Equations
theorem finsupp.lt_of_forall_lt_of_lt {α : Type u_1} {N : Type u_2} [has_zero N] [linear_order α] [partial_order N] (a b : lex →₀ N)) (i : α) :
( (j : α), j < i (of_lex a) j = (of_lex b) j) (of_lex a) i < (of_lex b) i a < b

We are about to sneak in a hypothesis that might appear to be too strong. We assume covariant_class 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.zero_divisors_in_add_monoid_algebras for a counterexample.