English
Let p: ℕ → Prop. If for the given n, every finite subset hf of setOf p satisfies n < #hf.toFinset, then p(nth p n).
Русский
Пусть p: ℕ → ⊤. Если для данного n выполняется, что для каждого конечного подмножества hf множества {x | p x} верно n < #hf.toFinset, то p(nth p n).
LaTeX
$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ (\\\\forall hf:\\\\{x:\\\\mathbb{N}\\\\mid p x\\\\}\\\\Finite,\\\\ n < #hf.toFinset) \\\\Rightarrow \\\\ p(\\\\mathrm{nth}\\\\ p\\\\ n).$$$
Lean4
theorem nth_mem (n : ℕ) (h : ∀ hf : (setOf p).Finite, n < #hf.toFinset) : p (nth p n) :=
(setOf p).finite_or_infinite.elim (fun hf => nth_mem_of_lt_card hf (h hf)) fun h => nth_mem_of_infinite h n
