Pi.lex_desc
theorem Pi.lex_desc :
∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : DecidableEq ι] [inst_2 : Preorder α] {f : ι → α}
{i j : ι}, i ≤ j → f j < f i → toLex (f ∘ ⇑(Equiv.swap i j)) < toLex f
This theorem states that if we have a function `f` from a type `ι` to `α` (with both types having a predefined order), and we swap the values `f` gives at two points `i` and `j` such that `i` is less than or equal to `j` and `f(j)` is strictly less than `f(i)`, then the lexicographic order of the new function (after swapping) is strictly less than that of the original function. That is, in terms of lexicographic order, rearranging a strictly decreasing pair in a function makes it "smaller".
More concisely: If `f: ι → α` is a function with types `ι` and `α` having a predefined order, and `i ≤ j` with `f(j) < f(i)`, then the function `x => if x = i then f(j) else if x = j then f(i) else f x` has a strictly smaller lexicographic order than `f`.
|
Pi.toLex_strictMono
theorem Pi.toLex_strictMono :
∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : IsWellOrder ι fun x x_1 => x < x_1]
[inst_2 : (i : ι) → PartialOrder (β i)], StrictMono ⇑toLex
The theorem `Pi.toLex_strictMono` states that for all types `ι` with a linear order and well-order properties, and all type families `β` indexed by `ι` with a partial order on each type, the function `toLex`, which is an identity function on `Lex` of a type, is strictly monotone. In other words, if `a` and `b` are elements of `ι` and `a < b`, then `toLex(a) < toLex(b)`. This suggests that `toLex` preserves the order of elements, which is a key property for many mathematical structures and algorithms.
More concisely: For any type `ι` with linear and well-order properties, and type family `β` over `ι` with a partial order, the function `toLex : ι → Lex β` is strictly monotone with respect to the linear order on `ι`.
|