tendsto_add_atTop_iff_nat — Mathlib

English

For a fixed k ∈ ℕ, the tail shift f(n) ↦ f(n + k) has the same convergence along atTop as f itself.

Русский

Для фиксированного k ∈ ℕ сдвиг по индексу на k не меняет сходимость вдоль atTop: Tendsto f(n + k) к l эквивалентно Tendsto f к l.

LaTeX

$$$$\operatorname{Tendsto}\bigl(\lambda n. f(n + k)\bigr)\;\operatorname{atTop}\; l \iff \operatorname{Tendsto} f\;\operatorname{atTop}\; l$$$$

Lean4

theorem tendsto_add_atTop_iff_nat {f : ℕ → α} {l : Filter α} (k : ℕ) :
    Tendsto (fun n => f (n + k)) atTop l ↔ Tendsto f atTop l :=
  show Tendsto (f ∘ fun n => n + k) atTop l ↔ Tendsto f atTop l by rw [← tendsto_map'_iff, map_add_atTop_eq_nat]

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