English
Let m ≤ n. If for all finite hf : (setOf p).Finite we have n < #hf.toFinset, then nth p m ≤ nth p n.
Русский
Пусть m ≤ n. Если для всех конечных hf : (setOf p).Finite выполняется n < #hf.toFinset, тогда nth p m ≤ nth p n.
LaTeX
$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ {m\\\\ n}:\\\\mathbb{N},\\\\ m\\\\le\\\\ n \\\\Rightarrow \\\\ (\\\\forall hf:\\\\{x:\\\\mathbb{N}\\\\mid p x\\\\}\\\\Finite,\\\\ n < #hf.toFinset) \\\\Rightarrow \\\\mathrm{nth}\\\\ p\\\\ m \\\\le \\\\mathrm{nth}\\\\ p\\\\ n.$$$
Lean4
theorem nth_le_nth' {m n : ℕ} (hle : m ≤ n) (h : ∀ hf : (setOf p).Finite, n < #hf.toFinset) : nth p m ≤ nth p n :=
(setOf p).finite_or_infinite.elim (fun hf => nth_le_nth_of_lt_card hf hle (h _)) fun hf => (nth_le_nth hf).2 hle
