map_sort — Mathlib

English

If f preserves the order relation between all elements, applying f to a sorted multiset preserves sorting with the corresponding relation on β.

Русский

Если отображение f сохраняет порядок между любыми двумя элементами, применение f к отсортированному мультсетy сохраняет упорядочение по relation r'.

LaTeX

$$$$ (s.sort r).\\,\\!\\map f = (s.\\!map f).sort r' $$$$

Lean4

theorem map_sort (f : α → β) (s : Multiset α) (hs : ∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b)) :
    (s.sort r).map f = (s.map f).sort r' := by
  revert s
  exact Quot.ind fun l h => map_mergeSort (l := l) (by simpa using h)

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