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 → α i → Prop) (x : Π₀ (i : ι), α i) (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 (· < ·) (· < ·).

theorem Pi.lex_eq_dfinsupp_lex {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} (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 → α i → Prop} {a : Π₀ (i : ι), α i} {b : Π₀ (i : ι), α i} : DFinsupp.Lex r s a b ↔ ∃ j, (∀ (d : ι), r d j → ↑a 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) [IsStrictOrder ι r] {x : Π₀ (i : ι), α i} {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 : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] (r : ι → ι → Prop) [IsStrictOrder ι r] {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)] [LinearOrder ι] [(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)] [LinearOrder ι] [(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)] [LinearOrder ι] [(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 g → False)

@[irreducible]

def DFinsupp.Lex.decidableLE {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : DecidableRel fun x x_1 => x ≤ x_1

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

@[irreducible]

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

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

theorem DFinsupp.Lex.decidableLT_def {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : DFinsupp.Lex.decidableLT = DFinsupp.lt_trichotomy_rec (fun {f g} h => isTrue 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)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : DecidableEq (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.linearOrder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(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)] [LinearOrder ι] [(i : ι) → PartialOrder (α i)] : Monotone ↑toLex

theorem DFinsupp.lt_of_forall_lt_of_lt {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(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) i → a < 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} [LinearOrder ι] [(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} [LinearOrder ι] [(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} [LinearOrder ι] [(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} [LinearOrder ι] [(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} [LinearOrder ι] [(i : ι) → CanonicallyOrderedAddMonoid (α i)] : OrderBot (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.orderedAddCancelCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (α i)] : OrderedCancelAddCommMonoid (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.orderedAddCommGroup {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedAddCommGroup (α i)] : OrderedAddCommGroup (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.linearOrderedCancelAddCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] : LinearOrderedCancelAddCommMonoid (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.linearOrderedAddCommGroup {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → LinearOrderedAddCommGroup (α i)] : LinearOrderedAddCommGroup (Lex (Π₀ (i : ι), α i))