extraction_forall_of_eventually' — Mathlib

English

If for every n there exists N such that P(n,k) holds for all k ≥ N, then there exists a strictly increasing φ with P(n,φ(n)).

Русский

Если для каждого n существует N такой, что P(n,k) выполняется для всех k ≥ N, тогда существует строго возрастающая φ, для которой P(n,φ(n)).

LaTeX

$$$\forall P:\mathbb{N}\to\mathbb{N}\to Prop,\ (\forall n,\exists N,\forall k≥N,\ P(n,k))\Rightarrow \exists φ:\mathbb{N}\to\mathbb{N},\ StrictMono(φ) \land ∀ n, P(n,φ(n))$$$

Lean4

theorem extraction_forall_of_eventually' {P : ℕ → ℕ → Prop} (h : ∀ n, ∃ N, ∀ k ≥ N, P n k) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P n (φ n) :=
  extraction_forall_of_eventually (by simp [eventually_atTop, h])

Похожие утверждения