comp_perm_comp_sort_eq_comp_sort — Mathlib

English

The sorted versions of f and of any permutation f ∘ σ agree: (f ∘ σ) ∘ sort (f ∘ σ) = f ∘ sort f.

Русский

Упорядоченные версии f и любой перестановки f ∘ σ совпадают: (f ∘ σ) ∘ sort (f ∘ σ) = f ∘ sort f.

LaTeX

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

Lean4

/-- The sorted versions of a tuple `f` and of any permutation of `f` agree. -/
theorem comp_perm_comp_sort_eq_comp_sort : (f ∘ σ) ∘ sort (f ∘ σ) = f ∘ sort f :=
  by
  rw [Function.comp_assoc, ← Equiv.Perm.coe_mul]
  exact unique_monotone (monotone_sort (f ∘ σ)) (monotone_sort f)

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