English
If for every n, the relation P(n,k) holds frequently as k→∞, then there exists a strictly increasing φ with P(n,φ(n)) for all n.
Русский
Если для каждого n отношение P(n,k) часто выполняется при k→∞, то существует строго возрастающая φ такая, что P(n,φ(n)) выполняется для всех n.
LaTeX
$$$\forall P:\mathbb{N}\to\mathbb{N}\to Prop,\ (\forall n,\text{Frequently}(k\mapsto P(n,k))\ AT\ Top)\Rightarrow \exists φ:\mathbb{N}\to\mathbb{N},\ StrictMono(φ) \land \forall n, P(n,φ(n))$$$
Lean4
theorem extraction_forall_of_frequently {P : ℕ → ℕ → Prop} (h : ∀ n, ∃ᶠ k in atTop, P n k) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P n (φ n) :=
by
simp only [frequently_atTop'] at h
choose u hu hu' using h
use (fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v : ℕ → ℕ)
constructor
· apply strictMono_nat_of_lt_succ
intro n
apply hu
· intro n
cases n <;> simp [hu']
