English
If we swap two indices i and j in a function f: ι → α with i ≤ j and f(j) < f(i), then the lexicographic value of the swapped function is strictly smaller than that of the original.
Русский
Если поменять местами две позиции i и j в функции f: ι → α, причём i ≤ j и f(j) < f(i), то лексикографическое значение полученной функции станет строго меньше исходного.
LaTeX
$$$\mathrm{toLex}(f \circ \mathrm{swap}(i,j)) < \mathrm{toLex}(f)$$$
Lean4
/-- If we swap two strictly decreasing values in a function, then the result is lexicographically
smaller than the original function. -/
theorem lex_desc {α} [Preorder ι] [DecidableEq ι] [LT α] {f : ι → α} {i j : ι} (h₁ : i ≤ j) (h₂ : f j < f i) :
toLex (f ∘ Equiv.swap i j) < toLex f :=
⟨i, fun _ hik => congr_arg f (Equiv.swap_apply_of_ne_of_ne hik.ne (hik.trans_le h₁).ne), by
simpa only [Pi.toLex_apply, Function.comp_apply, Equiv.swap_apply_left] using h₂⟩
