English
For a property P: ℕ → Prop such that for every N there exists n > N with P(n), there exists an increasing sequence φ: ℕ → ℕ with StrictMono and P(φ(n)) for all n.
Русский
Для свойства P: ℕ → Prop, удовлетворяющего условию существования большего индекса с P(n) для любого N, существует строго возрастающая подпоследовательность φ: ℕ → ℕ с P(φ(n)) для всех n.
LaTeX
$$$\\forall P : \\mathbb{N} \\to \\mathrm{Prop}, (\\forall N, \\exists n > N, P n) \\Rightarrow \\exists \\phi : \\mathbb{N} \\to \\mathbb{N}, \\mathrm{StrictMono} \\phi \\land \\forall n, P (\\phi n)$$$
Lean4
theorem exists_strictMono_subsequence {P : ℕ → Prop} (h : ∀ N, ∃ n > N, P n) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P (φ n) :=
by
have : NoMaxOrder { n // P n } := ⟨fun n ↦ Exists.intro ⟨(h n.1).choose, (h n.1).choose_spec.2⟩ (h n.1).choose_spec.1⟩
obtain ⟨f, hf, _⟩ := Nat.exists_strictMono' (⟨(h 0).choose, (h 0).choose_spec.2⟩ : { n // P n })
exact Exists.intro (fun n ↦ (f n).1) ⟨hf, fun n ↦ (f n).2⟩
