nth_eq_getD_sort — Mathlib

English

If p defines a finite set hf, then nth p n equals the n-th element of the sorted hf.toFinset (using the natural order), i.e., nth p n = the n-th smallest element of {k : p(k)} or 0 if out of range.

Русский

Если p задаёт конечное множество hf, то nth p n равно n-му элементу отсортированного hf.toFinset (по естественному порядку), то есть n-му наименьшему элементу {k | p(k)}, или 0, если такого элемента нет.

LaTeX

$$If hf is finite, then nth p n = (hf.toFinset.sort (≤)).getD n 0.$$

Lean4

theorem nth_eq_getD_sort (h : (setOf p).Finite) (n : ℕ) : nth p n = (h.toFinset.sort (· ≤ ·)).getD n 0 :=
  dif_pos h

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