comp_sort_eq_comp_iff_monotone — Mathlib

English

For any permutation σ, f ∘ σ = f ∘ sort f if and only if f ∘ σ is monotone.

Русский

Для любой перестановки σ верно: f ∘ σ = f ∘ sort f тогда и только тогда, когда f ∘ σ монотонна.

LaTeX

$$$(f \\circ σ) = (f \\circ \\mathrm{sort}(f)) \\iff \\mathrm{Monotone}(f \\circ σ).$$$

Lean4

/-- A permutation of a tuple `f` is `f` sorted if and only if it is monotone. -/
theorem comp_sort_eq_comp_iff_monotone : f ∘ σ = f ∘ sort f ↔ Monotone (f ∘ σ) :=
  ⟨fun h => h.symm ▸ monotone_sort f, fun h => unique_monotone h (monotone_sort f)⟩

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