English
If we swap two strictly increasing values in a function, then the result is smaller in colex order: toColex(f ∘ swap(i,j)) < toColex(f) when i ≤ j and f(i) < f(j).
Русский
Если поменять две строго возрастающие величины в функции, то результат меньше в ко-лексическом порядке: toColex(f ∘ swap(i,j)) < toColex(f) при i ≤ j и f(i) < f(j).
LaTeX
$$$\mathrm{toColex}(f \circ \mathrm{swap}(i,j)) < \mathrm{toColex}(f) \quad \text{if } i \le j \text{ and } f(i) < f(j)$$$
Lean4
/-- If we swap two strictly increasing values in a function, then the result is colexicographically
smaller than the original function. -/
theorem colex_asc {α} [Preorder ι] [DecidableEq ι] [LT α] {f : ι → α} {i j : ι} (h₁ : i ≤ j) (h₂ : f i < f j) :
toColex (f ∘ Equiv.swap i j) < toColex f := by
rw [Equiv.swap_comm]
exact lex_desc (ι := ιᵒᵈ) h₁ h₂
