mathlib3 documentation

data.finsupp.lex

Lexicographic order on finitely supported functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the lexicographic order on finsupp.

source
@[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
source
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
source
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)
source
theorem finsupp.lex_eq_inv_image_dfinsupp_lex {α : Type u_1} {N : Type u_2} [has_zero N] (r : α → α → Prop) (s : N → N → Prop) :
finsupp.lex r s = inv_image (dfinsupp.lex r (λ (a : α), s)) finsupp.to_dfinsupp
source
@[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
source
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
source
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
source
@[protected, instance]
def finsupp.lex.is_strict_order {α : Type u_1} {N : Type u_2} [has_zero N] [linear_order α] [partial_order N] :
is_strict_order (lex (α →₀ N)) has_lt.lt
source
@[protected, instance]
def finsupp.lex.partial_order {α : Type u_1} {N : Type u_2} [has_zero N] [linear_order α] [partial_order N] :
partial_order (lex (α →₀ 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
source
@[protected, instance]
def finsupp.lex.linear_order {α : Type u_1} {N : Type u_2} [has_zero N] [linear_order α] [linear_order N] :
linear_order (lex (α →₀ N))

The linear order on finsupps obtained by the lexicographic ordering.

Equations
source
theorem finsupp.to_lex_monotone {α : Type u_1} {N : Type u_2} [has_zero N] [linear_order α] [partial_order N] :
monotone ⇑to_lex
source
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.

source
@[protected, instance]
def finsupp.lex.covariant_class_lt_left {α : Type u_1} {N : Type u_2} [linear_order α] [add_monoid N] [linear_order N] [covariant_class N N has_add.add has_lt.lt] :
covariant_class (lex (α →₀ N)) (lex (α →₀ N)) has_add.add has_lt.lt
source
@[protected, instance]
def finsupp.lex.covariant_class_le_left {α : Type u_1} {N : Type u_2} [linear_order α] [add_monoid N] [linear_order N] [covariant_class N N has_add.add has_lt.lt] :
covariant_class (lex (α →₀ N)) (lex (α →₀ N)) has_add.add has_le.le
source
@[protected, instance]
def finsupp.lex.covariant_class_lt_right {α : Type u_1} {N : Type u_2} [linear_order α] [add_monoid N] [linear_order N] [covariant_class N N (function.swap has_add.add) has_lt.lt] :
covariant_class (lex (α →₀ N)) (lex (α →₀ N)) (function.swap has_add.add) has_lt.lt
source
@[protected, instance]
def finsupp.lex.covariant_class_le_right {α : Type u_1} {N : Type u_2} [linear_order α] [add_monoid N] [linear_order N] [covariant_class N N (function.swap has_add.add) has_lt.lt] :
covariant_class (lex (α →₀ N)) (lex (α →₀ N)) (function.swap has_add.add) has_le.le