Theorems · Theorem · order theory

Pi.lex_desc

∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : DecidableEq ι] [inst_2 : LT α] {f : ι → α} {i j : ι},
  i ≤ j → f j < f i → toLex (f ∘ ⇑(Equiv.swap i j)) < toLex f

If we swap two strictly decreasing values in a function, then the result is lexicographically smaller than the original function.

Defined in

Mathlib.Order.PiLex

Cited by

2 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderDecidableEqLT