antitone_pair_of_not_sorted' — Mathlib

English

If f ∘ σ ≠ f ∘ sort f, then there exists i < j with (f ∘ σ) j < (f ∘ σ) i.

Русский

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

LaTeX

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

Lean4

/-- If a permutation `f ∘ σ` of 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 :=
  by
  contrapose! h
  exact comp_sort_eq_comp_iff_monotone.mpr (monotone_iff_forall_lt.mpr h)

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