filter_range_nth_eq_insert_of_infinite

English

If the truth-set {n | p(n)} is infinite, then for every k, {n ∈ range(nth p (k+1)) | p n} equals insert(nth p k) ({n ∈ range(nth p k) | p n}).

Русский

Если множество истности бесконечно, то для каждого k выполняется равенство: {n ∈ range(nth p (k+1)) | p n} = insert(nth p k) ({n ∈ range(nth p k) | p n}).

LaTeX

$$$$\\{n\\in \\mathrm{range}(\\mathrm{nth}\,p(k+1)) \\mid p(n)\\} = \\mathrm{insert}(\\mathrm{nth}\,p(k), \\{n\\in \\mathrm{range}(\\mathrm{nth}\,p(k)) \\mid p(n)\\})$$$$

Lean4

theorem filter_range_nth_eq_insert_of_infinite (hp : (setOf p).Infinite) (k : ℕ) :
    {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 hf => absurd hf hp

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