English
For any p: ℕ → Prop, if n satisfies n < #hf.toFinset for all hf : (setOf p).Finite, then n ≤ nth p n.
Русский
Для любого p: ℕ → ⊤, если для всех hf : (setOf p).Finite выполнено n < #hf.toFinset, тогда n ≤ nth p n.
LaTeX
$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ {n}:\\\\mathbb{N},\\\\ (\\\\forall hf:\\\\{x:\\\\mathbb{N}\\\\mid p x\\\\}\\\\Finite,\\\\ n < #hf.toFinset) \\\\Rightarrow \\\\ n \\\\le \\\\mathrm{nth}\\\\ p\\\\ n.$$$
Lean4
theorem le_nth {n : ℕ} (h : ∀ hf : (setOf p).Finite, n < #hf.toFinset) : n ≤ nth p n :=
(setOf p).finite_or_infinite.elim
(fun hf => ((nth_strictMonoOn hf).mono <| Set.Iic_subset_Iio.2 (h _)).Iic_id_le _ le_rfl) fun hf =>
(nth_strictMono hf).id_le _
