antitone_pair_of_not_sorted — Mathlib

English

If f ≠ f ∘ sort f, then there exist i < j with f j < f i.

Русский

Если f не равно f ∘ sort f, то существуют i<j такие, что f j < f i.

LaTeX

$$$\\exists i,j,\\ i

Lean4

/-- If the tuple `f` is not the same as `f ∘ sort f`, then `f` has a pair of strictly decreasing
entries. -/
theorem antitone_pair_of_not_sorted (h : f ≠ f ∘ sort f) : ∃ i j, i < j ∧ f j < f i :=
  antitone_pair_of_not_sorted' (id h : f ∘ Equiv.refl _ ≠ _)

Похожие утверждения