English
A permutation σ equals sort f if and only if the map σ followed by graphEquiv₁ f is strictly monotone.
Русский
Перестановка σ равна sort f тогда и только тогда, когда отображение σ, затем graphEquiv₁ f, строго монотонно.
LaTeX
$$$\\sigma = \\mathrm{sort}(f) \\iff \\mathrm{StrictMono}(\\sigma \\circ \\mathrm{graphEquiv}_1(f)).$$$
Lean4
/-- A permutation `σ` equals `sort f` if and only if the map `i ↦ (f (σ i), σ i)` is
strictly monotone (w.r.t. the lexicographic ordering on the target). -/
theorem eq_sort_iff' : σ = sort f ↔ StrictMono (σ.trans <| graphEquiv₁ f) :=
by
constructor <;> intro h
· rw [h, sort, Equiv.trans_assoc, Equiv.symm_trans_self]
exact (graphEquiv₂ f).strictMono
· have := Subsingleton.elim (graphEquiv₂ f) (h.orderIsoOfSurjective _ <| Equiv.surjective _)
ext1 x
exact (graphEquiv₁ f).apply_eq_iff_eq_symm_apply.1 (DFunLike.congr_fun this x).symm
