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 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 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 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.instLTLex {ι : 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 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 y : Π₀ (i : ι), α i} (hlt : x < y) : Pi.Lex r (fun {i : ι} (x1 x2 : α i) => x1 < x2) ⇑x ⇑y

instance DFinsupp.Lex.isStrictOrder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → PartialOrder (α i)] : IsStrictOrder (Lex (Π₀ (i : ι), α i)) fun (x1 x2 : Lex (Π₀ (i : ι), α i)) => x1 < x2

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)] : decidableLE = DFinsupp.lt_trichotomy_rec✝ (fun {f g : Π₀ (i : ι), α i} (h : toLex f < toLex g) => isTrue ⋯) (fun {f g : Π₀ (i : ι), α i} (h : toLex f = toLex g) => isTrue ⋯) fun {f g : Π₀ (i : ι), α i} (h : toLex g < toLex f) => isFalse ⋯

@[irreducible]

def DFinsupp.Lex.decidableLE {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : DecidableLE (Lex (Π₀ (i : ι), α i))

The less-or-equal 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)] : decidableLT = DFinsupp.lt_trichotomy_rec✝ (fun {f g : Π₀ (i : ι), α i} (h : toLex f < toLex g) => isTrue h) (fun {f g : Π₀ (i : ι), α i} (h : toLex f = toLex g) => isFalse ⋯) fun {f g : Π₀ (i : ι), α i} (h : toLex g < toLex f) => isFalse ⋯

@[irreducible]

def DFinsupp.Lex.decidableLT {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] : DecidableLT (Lex (Π₀ (i : ι), α i))

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

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 b : Lex (Π₀ (i : ι), α i)) (i : ι) : (∀ 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 AddLeftStrictMono (covariant 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.addLeftStrictMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)] : AddLeftStrictMono (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.addLeftMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)] : AddLeftMono (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.addRightStrictMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)] : AddRightStrictMono (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.addRightMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)] : AddRightMono (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.orderBot {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] : OrderBot (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.isOrderedCancelAddMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedCancelAddMonoid (α i)] : IsOrderedCancelAddMonoid (Lex (Π₀ (i : ι), α i))

instance DFinsupp.Lex.isOrderedAddMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddCommGroup (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedAddMonoid (α i)] : IsOrderedAddMonoid (Lex (Π₀ (i : ι), α i))