English
For a predicate p on ℕ and any k, the set {n ∈ range(nth p (k+1)) | p n} is a subset of insert(nth p k) of {n ∈ range(nth p k) | p n}. In words, the elements satisfying p up to the (k+1)-st true value are either the k-th true value or lie among earlier true values.
Русский
Для предиката p на ℕ и любого k множество {n ∈ range(nth p (k+1)) | p n} является подмножеством вставки nth p k в множество {n ∈ range(nth p k) | p n}. Иными словами, элементы, удовлетворяющие p до (k+1)-го истинного значения, либо равны k-му истинному значению, либо принадлежат более ранним истинным значениям.
LaTeX
$$$\\{n : n \\in \\mathrm{range}(\\mathrm{nth}\,p(k+1)) \\mid p(n)\\} \\subseteq \\{\\,\\mathrm{nth}\,p(k)\\} \\cup \\{n : n \\in \\mathrm{range}(\\mathrm{nth}\,p(k)) \\mid p(n)\\}$$$
Lean4
theorem filter_range_nth_subset_insert (k : ℕ) :
{n ∈ range (nth p (k + 1)) | p n} ⊆ insert (nth p k) ({n ∈ range (nth p k) | p n}) :=
by
intro a ha
simp only [mem_insert, mem_filter, mem_range] at ha ⊢
exact (le_nth_of_lt_nth_succ ha.1 ha.2).eq_or_lt.imp_right fun h => ⟨h, ha.2⟩
