orderIsoOfFin_symm_apply — Mathlib

English

For x in s, the inverse image under the order isomorphism corresponds to the index of x in the sorted order.

Русский

Для x из s, отображение обратного порядка соответствует индексу x в отсортированном порядке.

LaTeX

$$$ \\uparrow((s.orderIsoOfFin h).symm x) = (s.sort (\\le)).idxOf \\uparrow x $$$

Lean4

theorem orderIsoOfFin_symm_apply (s : Finset α) {k : ℕ} (h : s.card = k) (x : s) :
    ↑((s.orderIsoOfFin h).symm x) = (s.sort (· ≤ ·)).idxOf ↑x :=
  rfl

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