eq_sort_iff — Mathlib

English

σ = sort f iff Monotone (f ∘ σ) and for all i<j, if f(σ i) = f(σ j) then σ i < σ j.

Русский

σ = sort f эквивалентно тому, что f ∘ σ монотонна и для любых i<j, если f(σ i) = f(σ j), то σ i < σ j.

LaTeX

$$$\\sigma = \\mathrm{sort}(f) \\iff \\Big( \\mathrm{Monotone}(f \\circ \\sigma) \\Big) \\land \\forall i,j,\\ i

Lean4

/-- A permutation `σ` equals `sort f` if and only if `f ∘ σ` is monotone and whenever `i < j`
and `f (σ i) = f (σ j)`, then `σ i < σ j`. This means that `sort f` is the lexicographically
smallest permutation `σ` such that `f ∘ σ` is monotone. -/
theorem eq_sort_iff : σ = sort f ↔ Monotone (f ∘ σ) ∧ ∀ i j, i < j → f (σ i) = f (σ j) → σ i < σ j :=
  by
  rw [eq_sort_iff']
  refine ⟨fun h => ⟨(monotone_proj f).comp h.monotone, fun i j hij hfij => ?_⟩, fun h i j hij => ?_⟩
  · exact ((Prod.Lex.toLex_lt_toLex.1 <| h hij).resolve_left hfij.not_lt).2
  · obtain he | hl := (h.1 hij.le).eq_or_lt <;> apply Prod.Lex.toLex_lt_toLex.2
    exacts [Or.inr ⟨he, h.2 i j hij he⟩, Or.inl hl]

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