orderEmbOfFin_apply — Mathlib

English

Let s be a finite subset of a linearly ordered set α with card k, and let i ∈ Fin k. Then s.orderEmbOfFin h i equals the i-th element of the sorted list of s, i.e., the i-th element of s.sort(≤).

Русский

Пусть s — конечное подмножество линейно упорядоченного множества α; кардинал равна k. Пусть i ∈ Fin k. Тогда s.orderEmbOfFin h i равно i-му элементу упорядоченного по возрастанию списка s, то есть i-му элементу списка s.sort(≤).

LaTeX

$$$s.orderEmbOfFin\,h\,i = (s.sort(\le))\,[i]^{\prime}$$$

Lean4

theorem orderEmbOfFin_apply (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k) :
    s.orderEmbOfFin h i = (s.sort (· ≤ ·))[i]'(by rw [length_sort, h]; exact i.2) :=
  rfl

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