English
Assume a predicate p with decidable truth, and that the finite range property holds with a bound k+1 < card of the finite set. Then the set of n with p(n) in range(nth p (k+1)) equals insert(nth p k) of {n ∈ range(nth p k) | p n}. In other words, adding nth p k to the previous layer accounts for the next layer.
Русский
Пусть предикат p имеет разрешимость истинности, и выполняется условие конечности диапазона с верхней гранью. Тогда множество n с p(n) внутри range(nth p(k+1)) равно вставке nth p k в множество {n ∈ range(nth p k) | p n}. Иными словами, добавление k-го истинного значения покрывает следующий слой.
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 {k : ℕ} (hlt : ∀ hf : (setOf p).Finite, k + 1 < #hf.toFinset) :
{n ∈ range (nth p (k + 1)) | p n} = insert (nth p k) ({n ∈ range (nth p k) | p n}) :=
by
refine (filter_range_nth_subset_insert p k).antisymm fun a ha => ?_
simp only [mem_insert, mem_filter, mem_range] at ha ⊢
have : nth p k < nth p (k + 1) := nth_lt_nth' k.lt_succ_self hlt
rcases ha with (rfl | ⟨hlt, hpa⟩)
· exact ⟨this, nth_mem _ fun hf => k.lt_succ_self.trans (hlt hf)⟩
· exact ⟨hlt.trans this, hpa⟩
