sort_eq_refl_iff_monotone — Mathlib

English

The sort is the identity if and only if f is monotone.

Русский

Сортировка совпадает с идентичностью тогда и только тогда, когда f монотонна.

LaTeX

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

Lean4

/-- The permutation that sorts `f` is the identity if and only if `f` is monotone. -/
theorem sort_eq_refl_iff_monotone : sort f = Equiv.refl _ ↔ Monotone f :=
  by
  rw [eq_comm, eq_sort_iff, Equiv.coe_refl, Function.comp_id]
  simp only [id, and_iff_left_iff_imp]
  exact fun _ _ _ hij _ => hij

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