English
Let p be a property on natural numbers such that the set {n ∈ ℕ | p(n)} is infinite. Then the sequence k ↦ nth p k is strictly increasing, i.e. nth p k < nth p n if and only if k < n.
Русский
Пусть p : ℕ → ℕ→Prop так, что множество {n ∈ ℕ | p(n)} бесконечно. Тогда последовательность k ↦ nth p k строго возрастает: nth p k < nth p n тогда и только тогда, когда k < n.
LaTeX
$$$\\forall {p : \\mathbb{N} \\to \\mathbb{P}}, (\\{ n \\in \\mathbb{N} \\mid p(n) \\} \\text{ Infinite}) \\to \\forall {k n \\in \\mathbb{N}},\\; \\operatorname{nth} p k < \\operatorname{nth} p n \\iff k < n$$$
Lean4
theorem nth_lt_nth (hf : (setOf p).Infinite) {k n} : nth p k < nth p n ↔ k < n :=
(nth_strictMono hf).lt_iff_lt
