strictMono_subseq_of_id_le — Mathlib

English

If u:ℕ→ℕ satisfies n ≤ u(n) for all n, then there exists a strictly increasing φ with u ∘ φ strictly increasing.

Русский

Если u(n) ≥ n для всех n, существует строгая подпоследовательность φ с тем, что u∘φ строго возрастает.

LaTeX

$$$\forall n, n \le u(n) \Rightarrow \exists φ: \mathbb{N} \to \mathbb{N}, \ StrictMono φ \land \ StrictMono(u \circ φ)$$$

Lean4

theorem strictMono_subseq_of_id_le {u : ℕ → ℕ} (hu : ∀ n, n ≤ u n) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ StrictMono (u ∘ φ) :=
  strictMono_subseq_of_tendsto_atTop (tendsto_atTop_mono hu tendsto_id)

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