tendsto_atTop' — Mathlib

English

If P(n) holds eventually in atTop, there exists a strictly increasing φ such that P(φ(n)) holds for all n.

Русский

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

LaTeX

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

Lean4

theorem tendsto_atTop' : Tendsto f atTop l ↔ ∀ s ∈ l, ∃ a, ∀ b ≥ a, f b ∈ s := by
  simp only [tendsto_def, mem_atTop_sets, mem_preimage]

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