# Documentation

Mathlib.Data.DFinsupp.Lex

# Lexicographic order on finitely supported dependent functions #

This file defines the lexicographic order on DFinsupp.

def DFinsupp.Lex {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] (r : ιιProp) (s : (i : ι) → α iα iProp) (x : Π₀ (i : ι), α i) (y : Π₀ (i : ι), α i) :

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

Instances For
theorem Pi.lex_eq_dfinsupp_lex {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] {r : ιιProp} {s : (i : ι) → α iα iProp} (a : Π₀ (i : ι), α i) (b : Π₀ (i : ι), α i) :
Pi.Lex r (fun {i} => s i) a b = DFinsupp.Lex r s a b
theorem DFinsupp.lex_def {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] {r : ιιProp} {s : (i : ι) → α iα iProp} {a : Π₀ (i : ι), α i} {b : Π₀ (i : ι), α i} :
DFinsupp.Lex r s a b j, (∀ (d : ι), r d ja d = b d) s j (a j) (b j)
instance DFinsupp.instLTLexDFinsupp {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [LT ι] [(i : ι) → LT (α i)] :
LT (Lex (Π₀ (i : ι), α i))
theorem DFinsupp.lex_lt_of_lt_of_preorder {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] (r : ιιProp) [] {x : Π₀ (i : ι), α i} {y : Π₀ (i : ι), α i} (hlt : x < y) :
i, (∀ (j : ι), r j ix j y j y j x j) x i < y i
theorem DFinsupp.lex_lt_of_lt {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] (r : ιιProp) [] {x : Π₀ (i : ι), α i} {y : Π₀ (i : ι), α i} (hlt : x < y) :
Pi.Lex r (fun {i} x x_1 => x < x_1) x y
instance DFinsupp.Lex.isStrictOrder {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [] [(i : ι) → PartialOrder (α i)] :
IsStrictOrder (Lex (Π₀ (i : ι), α i)) fun x x_1 => x < x_1
instance DFinsupp.Lex.partialOrder {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [] [(i : ι) → PartialOrder (α i)] :
PartialOrder (Lex (Π₀ (i : ι), α i))

The partial order on DFinsupps obtained by the lexicographic ordering. See DFinsupp.Lex.linearOrder for a proof that this partial order is in fact linear.

theorem DFinsupp.Lex.decidableLE_def {ι : Type u_3} {α : ιType u_4} [(i : ι) → Zero (α i)] [] [(i : ι) → LinearOrder (α i)] :
DFinsupp.Lex.decidableLE = DFinsupp.lt_trichotomy_rec (fun {f g} h => isTrue (_ : ↑(ofLex (toLex f)) = ↑(ofLex (toLex g)) toLex f < toLex g)) (fun {f g} h => isTrue (_ : ↑(ofLex (toLex f)) = ↑(ofLex (toLex g)) toLex f < toLex g)) fun {f g} h => isFalse (_ : toLex f toLex gFalse)
@[irreducible]
def DFinsupp.Lex.decidableLE {ι : Type u_3} {α : ιType u_4} [(i : ι) → Zero (α i)] [] [(i : ι) → LinearOrder (α i)] :
DecidableRel fun x x_1 => x x_1

The less-or-equal relation for the lexicographic ordering is decidable.

Instances For
@[irreducible]
def DFinsupp.Lex.decidableLT {ι : Type u_3} {α : ιType u_4} [(i : ι) → Zero (α i)] [] [(i : ι) → LinearOrder (α i)] :
DecidableRel fun x x_1 => x < x_1

The less-than relation for the lexicographic ordering is decidable.

Instances For
theorem DFinsupp.Lex.decidableLT_def {ι : Type u_3} {α : ιType u_4} [(i : ι) → Zero (α i)] [] [(i : ι) → LinearOrder (α i)] :
DFinsupp.Lex.decidableLT = DFinsupp.lt_trichotomy_rec (fun {f g} h => ) (fun {f g} h => isFalse (_ : ¬toLex f < toLex g)) fun {f g} h => isFalse (_ : ¬toLex f < toLex g)
instance DFinsupp.instDecidableEqLexDFinsupp {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [] [(i : ι) → LinearOrder (α i)] :
DecidableEq (Lex (Π₀ (i : ι), α i))
instance DFinsupp.Lex.linearOrder {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [] [(i : ι) → LinearOrder (α i)] :
LinearOrder (Lex (Π₀ (i : ι), α i))

The linear order on DFinsupps obtained by the lexicographic ordering.

theorem DFinsupp.toLex_monotone {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [] [(i : ι) → PartialOrder (α i)] :
Monotone toLex
theorem DFinsupp.lt_of_forall_lt_of_lt {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [] [(i : ι) → PartialOrder (α i)] (a : Lex (Π₀ (i : ι), α i)) (b : Lex (Π₀ (i : ι), α i)) (i : ι) :
(∀ (j : ι), j < i↑(ofLex a) j = ↑(ofLex b) j) → ↑(ofLex a) i < ↑(ofLex b) ia < b

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

instance DFinsupp.Lex.covariantClass_lt_left {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), CovariantClass (α i) (α i) (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
CovariantClass (Lex (Π₀ (i : ι), α i)) (Lex (Π₀ (i : ι), α i)) (fun x x_1 => x + x_1) fun x x_1 => x < x_1
instance DFinsupp.Lex.covariantClass_le_left {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), CovariantClass (α i) (α i) (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
CovariantClass (Lex (Π₀ (i : ι), α i)) (Lex (Π₀ (i : ι), α i)) (fun x x_1 => x + x_1) fun x x_1 => x x_1
instance DFinsupp.Lex.covariantClass_lt_right {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), CovariantClass (α i) (α i) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
CovariantClass (Lex (Π₀ (i : ι), α i)) (Lex (Π₀ (i : ι), α i)) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
instance DFinsupp.Lex.covariantClass_le_right {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), CovariantClass (α i) (α i) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
CovariantClass (Lex (Π₀ (i : ι), α i)) (Lex (Π₀ (i : ι), α i)) (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
instance DFinsupp.Lex.orderBot {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → ] :
OrderBot (Lex (Π₀ (i : ι), α i))
instance DFinsupp.Lex.orderedAddCancelCommMonoid {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → ] :
OrderedCancelAddCommMonoid (Lex (Π₀ (i : ι), α i))
instance DFinsupp.Lex.orderedAddCommGroup {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → OrderedAddCommGroup (α i)] :
OrderedAddCommGroup (Lex (Π₀ (i : ι), α i))
instance DFinsupp.Lex.linearOrderedCancelAddCommMonoid {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → ] :
LinearOrderedCancelAddCommMonoid (Lex (Π₀ (i : ι), α i))
instance DFinsupp.Lex.linearOrderedAddCommGroup {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → ] :
LinearOrderedAddCommGroup (Lex (Π₀ (i : ι), α i))