English
Let p: N → Prop and x with p x. Then there exists n such that nth p n = x and n is smaller than the cardinality of every finite subcollection of {n : p n}.
Русский
Пусть p: ℕ → ⊤ и есть x such что p x. Тогда существует n, для которого nth p n = x, и для каждого конечного подмножества F = {n : p n} выполняется n < |F|.
LaTeX
$$$\\\\forall x\\\\ (p x) \\\\Rightarrow \\\\exists n,\\\\ (\\\\forall hf:\\\\{m \\\\mid p m\\\\}\\\\text{ finite},\\\\ n < #hf.toFinset) \\\\land \\\\ (\\\\mathrm{nth}\\\\ p\\\\ n = x).$$$
Lean4
theorem exists_lt_card_nth_eq {x} (h : p x) : ∃ n, (∀ hf : (setOf p).Finite, n < #hf.toFinset) ∧ nth p n = x :=
by
refine (setOf p).finite_or_infinite.elim (fun hf => ?_) fun hf => ?_
· rcases exists_lt_card_finite_nth_eq hf h with ⟨n, hn, hx⟩
exact ⟨n, fun _ => hn, hx⟩
· rw [← @Set.mem_setOf_eq _ _ p, ← range_nth_of_infinite hf] at h
rcases h with ⟨n, hx⟩
exact ⟨n, fun hf' => absurd hf' hf, hx⟩
