English
If the predicate p has a finite truth-set, then for all k, the finite set {n ∈ range(nth p (k+1)) | p n} equals insert(nth p k) of {n ∈ range(nth p k) | p n}. The finite bound is given by the cardinality constraint.
Русский
Если множество истинности предиката p является конечным, то для каждого k множество {n ∈ range(nth p (k+1)) | p n} равно insert(nth p k) в {n ∈ range(nth p k) | p n}. Ограничение по кардинальности обеспечивает конечность.
LaTeX
$$$$\\{n:\\, n\\in \\mathrm{range}(\\mathrm{nth}\,p(k+1)) \\mid p(n)\\} = \\mathrm{insert}(\\mathrm{nth}\,p(k), \\{n:\\, n\\in \\mathrm{range}(\\mathrm{nth}\,p(k)) \\mid p(n)\\})$$$$
Lean4
theorem filter_range_nth_eq_insert_of_finite (hf : (setOf p).Finite) {k : ℕ} (hlt : k + 1 < #hf.toFinset) :
{n ∈ range (nth p (k + 1)) | p n} = insert (nth p k) ({n ∈ range (nth p k) | p n}) :=
filter_range_nth_eq_insert fun _ => hlt
