English
For any p: ℕ → Prop, if m < n and for all finite hf : (setOf p).Finite we have n < #hf.toFinset, then nth p m < nth p n.
Русский
Для любого p: ℕ → ⊤, если 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 < n \\\\Rightarrow \\\\ (\\\\forall hf:\\\\{x:\\\\mathbb{N}\\\\mid p x\\\\}\\\\Finite,\\\\ n < #hf.toFinset) \\\\Rightarrow \\\\ \\\\mathrm{nth}\\\\ p\\\\ m < \\\\mathrm{nth}\\\\ p\\\\ n.$$$
Lean4
theorem nth_lt_nth' {m n : ℕ} (hlt : 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_lt_nth_of_lt_card hf hlt (h _)) fun hf => (nth_lt_nth hf).2 hlt
