toFinset_sort — Mathlib

English

Let f be a linear-order-preserving embedding; then the same sort-map identity holds as in MapSort with StrictMonoOn hypothesis.

Русский

Пусть есть вложение, сохраняющее порядок; тогда равенство сортировки и отображения сохраняется при условии StrictMonoOn.

LaTeX

$$$ (s.sort (\\le)).map f = (s.map f).sort (\\le) $$$

Lean4

theorem _root_.List.toFinset_sort [DecidableEq α] {l : List α} (hl : l.Nodup) : sort r l.toFinset = l ↔ l.Sorted r :=
  by
  refine ⟨?_, List.eq_of_perm_of_sorted ((sort_perm_toList r _).trans (List.toFinset_toList hl)) (sort_sorted r _)⟩
  intro h
  rw [← h]
  exact sort_sorted r _

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