# Lexicographic order on finitely supported dependent functions #

This file defines the lexicographic order on `DFinsupp`.

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

Equations

- DFinsupp.Lex r s x y = Pi.Lex r (fun {i : ι} => s i) ⇑x ⇑y

Instances For

source
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
source
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)
source
instance DFinsupp.instLTLex {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LT ι] [(i : ι) → LT (α i)] :
LT (Lex (Π₀ (i : ι), α i))
Equations

- DFinsupp.instLTLex = { lt := fun (f g : Lex (Π₀ (i : ι), α i)) => DFinsupp.Lex (fun (x1 x2 : ι) => x1 < x2) (fun (x : ι) (x1 x2 : α x) => x1 < x2) (ofLex f) (ofLex g) }

source
theorem DFinsupp.lex_lt_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LT ι] [(i : ι) → LT (α i)] {a b : Lex (Π₀ (i : ι), α i)} :
a < b ↔ ∃ (i : ι), (∀ j < i, (ofLex a) j = (ofLex b) j) ∧ (ofLex a) i < (ofLex b) i
source
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
source
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
source
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
source
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 `DFinsupp`s obtained by the lexicographic ordering. See `DFinsupp.Lex.linearOrder` for a proof that this partial order is in fact linear.

Equations

- One or more equations did not get rendered due to their size.

source
instance DFinsupp.Lex.decidableLE {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] :
DecidableLE (Lex (Π₀ (i : ι), α i))

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

Equations

- One or more equations did not get rendered due to their size.

source
instance DFinsupp.Lex.decidableLT {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → LinearOrder (α i)] :
DecidableLT (Lex (Π₀ (i : ι), α i))

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

Equations

- One or more equations did not get rendered due to their size.

source
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 `DFinsupp`s obtained by the lexicographic ordering.

Equations

- One or more equations did not get rendered due to their size.

source
theorem DFinsupp.toLex_monotone {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [LinearOrder ι] [(i : ι) → PartialOrder (α i)] :
Monotone ⇑toLex
source
@[deprecated DFinsupp.lex_lt_iff (since := "2025-10-12")]
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`.

source
instance DFinsupp.Lex.addLeftStrictMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)] :
AddLeftStrictMono (Lex (Π₀ (i : ι), α i))
source
instance DFinsupp.Lex.addLeftMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)] :
AddLeftMono (Lex (Π₀ (i : ι), α i))
source
instance DFinsupp.Lex.addRightStrictMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)] :
AddRightStrictMono (Lex (Π₀ (i : ι), α i))
source
instance DFinsupp.Lex.addRightMono {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)] :
AddRightMono (Lex (Π₀ (i : ι), α i))
source
instance DFinsupp.Lex.orderBot {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] :
OrderBot (Lex (Π₀ (i : ι), α i))
Equations

- DFinsupp.Lex.orderBot = { bot := 0, bot_le := ⋯ }

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