map_sort — Mathlib

English

Let f be an embedding between types respecting a relation r and r'. Then sorting s in r and mapping by f equals sorting the image of s in r'.

Русский

Пусть f — вложение между типами, сохраняющее порядок между элементами множества s. Тогда сортировка s по r, затем отображение f, равна сортировке изображения s под f по r'.

LaTeX

$$$ (s\\!\\text{.sort } r).\\!map f = (s\\!\\text{.map } f).\\!sort r' $$$

Lean4

theorem map_sort (f : α ↪ β) (s : Finset α) (hs : ∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b)) :
    (s.sort r).map f = (s.map f).sort r' :=
  Multiset.map_sort _ _ _ _ hs

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