English
For every x in an infinite set s of natural numbers, there exists n ∈ ℕ such that x+n+1 ∈ s.
Русский
Для каждого x ∈ s, где s бесконечно, существует n ∈ ℕ такое, что x+n+1 ∈ s.
LaTeX
$$$\forall x\in s\;\exists n\in \mathbb{N},\ (x+n+1)\in s$$$
Lean4
theorem exists_succ (x : s) : ∃ n, (x : ℕ) + n + 1 ∈ s :=
by
by_contra h
have (a : ℕ) (ha : a ∈ s) : a < x + 1 :=
lt_of_not_ge fun hax => h ⟨a - (x + 1), by rwa [Nat.add_right_comm, Nat.add_sub_cancel' hax]⟩
classical
exact
Fintype.false
⟨(((Multiset.range (succ x)).filter (· ∈ s)).pmap (fun (y : ℕ) (hy : y ∈ s) => Subtype.mk y hy)
(by simp [-Multiset.range_succ])).toFinset,
by simpa [Subtype.ext_iff, Multiset.mem_filter, -Multiset.range_succ]⟩
