# mathlib3documentation

data.dfinsupp.lex

# Lexicographic order on finitely supported dependent 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 dfinsupp.

@[protected]
def dfinsupp.lex {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] (r : ι ι Prop) (s : Π (i : ι), α i α i Prop) (x y : Π₀ (i : ι), α i) :
Prop

dfinsupp.lex r s is the lexicographic relation on Π₀ i, α i, where ι is ordered by r, and α i is ordered by s i. The type synonym lex (Π₀ i, α i) has an order given by dfinsupp.lex (<) (λ i, (<)).

Equations
theorem pi.lex_eq_dfinsupp_lex {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] {r : ι ι Prop} {s : Π (i : ι), α i α i Prop} (a b : Π₀ (i : ι), α i) :
s a b = s a b
theorem dfinsupp.lex_def {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] {r : ι ι Prop} {s : Π (i : ι), α i α i Prop} {a b : Π₀ (i : ι), α i} :
s a b (j : ι), ( (d : ι), r d j a d = b d) s j (a j) (b j)
@[protected, instance]
def dfinsupp.lex.has_lt {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [has_lt ι] [Π (i : ι), has_lt (α i)] :
has_lt (lex (Π₀ (i : ι), α i))
Equations
theorem dfinsupp.lex_lt_of_lt_of_preorder {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [Π (i : ι), preorder (α i)] (r : ι ι Prop) [ r] {x y : Π₀ (i : ι), α i} (hlt : x < y) :
(i : ι), ( (j : ι), r j i x j y j y j x j) x i < y i
theorem dfinsupp.lex_lt_of_lt {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [Π (i : ι), partial_order (α i)] (r : ι ι Prop) [ r] {x y : Π₀ (i : ι), α i} (hlt : x < y) :
(λ (i : ι), has_lt.lt) x y
@[protected, instance]
def dfinsupp.lex.is_strict_order {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), partial_order (α i)] :
@[protected, instance]
def dfinsupp.lex.partial_order {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), partial_order (α i)] :
partial_order (lex (Π₀ (i : ι), α i))

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

Equations
@[protected, instance, irreducible]
def dfinsupp.lex.decidable_le {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), linear_order (α i)] :
Equations
@[protected, instance, irreducible]
def dfinsupp.lex.decidable_lt {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), linear_order (α i)] :
Equations
@[protected, instance]
def dfinsupp.lex.linear_order {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), linear_order (α i)] :
linear_order (lex (Π₀ (i : ι), α i))

The linear order on dfinsupps obtained by the lexicographic ordering.

Equations
theorem dfinsupp.to_lex_monotone {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), partial_order (α i)] :
theorem dfinsupp.lt_of_forall_lt_of_lt {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), partial_order (α i)] (a b : lex (Π₀ (i : ι), α i)) (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 (Π₀ i, α i) may fail to be monotone, when it is "just" monotone on α i.

@[protected, instance]
def dfinsupp.lex.covariant_class_lt_left {ι : Type u_1} {α : ι Type u_2} [linear_order ι] [Π (i : ι), add_monoid (α i)] [Π (i : ι), linear_order (α i)] [ (i : ι), covariant_class (α i) (α i) has_add.add has_lt.lt] :
covariant_class (lex (Π₀ (i : ι), α i)) (lex (Π₀ (i : ι), α i)) has_add.add has_lt.lt
@[protected, instance]
def dfinsupp.lex.covariant_class_le_left {ι : Type u_1} {α : ι Type u_2} [linear_order ι] [Π (i : ι), add_monoid (α i)] [Π (i : ι), linear_order (α i)] [ (i : ι), covariant_class (α i) (α i) has_add.add has_lt.lt] :
covariant_class (lex (Π₀ (i : ι), α i)) (lex (Π₀ (i : ι), α i)) has_add.add has_le.le
@[protected, instance]
def dfinsupp.lex.covariant_class_lt_right {ι : Type u_1} {α : ι Type u_2} [linear_order ι] [Π (i : ι), add_monoid (α i)] [Π (i : ι), linear_order (α i)] [ (i : ι), covariant_class (α i) (α i) has_lt.lt] :
covariant_class (lex (Π₀ (i : ι), α i)) (lex (Π₀ (i : ι), α i)) has_lt.lt
@[protected, instance]
def dfinsupp.lex.covariant_class_le_right {ι : Type u_1} {α : ι Type u_2} [linear_order ι] [Π (i : ι), add_monoid (α i)] [Π (i : ι), linear_order (α i)] [ (i : ι), covariant_class (α i) (α i) has_lt.lt] :
covariant_class (lex (Π₀ (i : ι), α i)) (lex (Π₀ (i : ι), α i)) has_le.le