listMap_orderEmbOfFin_finRange — Mathlib

English

The list obtained by mapping the i-th order-embedding over the finite range equals the sorted list of s.

Русский

Список, полученный отображением порядка достигнутого вложения, равен отсортированному списку s.

LaTeX

$$(List.finRange k).map (s.orderEmbOfFin h) = s.sort (<=)$$

Lean4

@[simp]
theorem listMap_orderEmbOfFin_finRange (s : Finset α) {k : ℕ} (h : s.card = k) :
    (List.finRange k).map (s.orderEmbOfFin h) = s.sort (· ≤ ·) :=
  by
  obtain rfl : k = (s.sort (· ≤ ·)).length := by simp [h]
  exact List.finRange_map_getElem (s.sort (· ≤ ·))

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