extraction_of_eventually_atTop — Mathlib

English

If P(n) holds eventually along atTop, then there exists a strictly increasing φ with P(φ(n)) for all n.

Русский

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

LaTeX

$$$\forall\!\!{P:N→Prop},\ (\forall^\infty n\ in\ atTop,\ P(n)) \Rightarrow \exists\ φ:\mathbb{N}→\mathbb{N},\ StrictMono(φ) \land \forall n, P(φ(n))$$$

Lean4

theorem extraction_of_eventually_atTop {P : ℕ → Prop} (h : ∀ᶠ n in atTop, P n) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P (φ n) :=
  extraction_of_frequently_atTop h.frequently

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