extraction_forall_of_eventually — Mathlib

English

If for every n, P(n,k) holds eventually in k, then there exists a strictly increasing φ with P(n,φ(n)) for all n.

Русский

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

LaTeX

$$$\forall P:\mathbb{N}\to\mathbb{N}\to Prop,\ (\forall n,\forall^\infty k\ in\ atTop,\ 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, ∀ᶠ k in atTop, P n k) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P n (φ n) :=
  extraction_forall_of_frequently fun n => (h n).frequently

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