map_finsetSort — Mathlib

English

If f is strictly monotone on a Finset s between α and β, then sorting s in α and mapping by f equals sorting the image in β with the same order.

Русский

Если f строго монотонна на Finset s между α и β, то сортировка s по α и отображение f дают такую же последовательность как сортировка образа в β по соответствующему порядку.

LaTeX

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

Lean4

theorem _root_.StrictMonoOn.map_finsetSort [LinearOrder α] [LinearOrder β] (f : α ↪ β) (s : Finset α)
    (hf : StrictMonoOn f s) : (s.sort (· ≤ ·)).map f = (s.map f).sort (· ≤ ·) :=
  Finset.map_sort _ _ _ _ fun _a ha _b hb => (hf.le_iff_le ha hb).symm

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