range_nth_of_finite — Mathlib

English

If hf is finite, then Range(nth p) = {0} ∪ setOf p.

Русский

Если hf конечное, то диапазон nth p равен {0} ∪ множество {x | p(x)}.

LaTeX

$$For hf finite, Set.range (nth p) = insert 0 (setOf p).$$

Lean4

theorem range_nth_of_finite (hf : (setOf p).Finite) : Set.range (nth p) = insert 0 (setOf p) := by
  simpa only [← List.getD_eq_getElem?_getD, ← nth_eq_getD_sort hf, mem_sort, Set.Finite.mem_toFinset] using
    Set.range_list_getD (hf.toFinset.sort (· ≤ ·)) 0

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