limsup_nat_add — Mathlib

English

For a sequence f: ℕ → α and a natural shift k, limsup of the shifted sequence equals limsup of the original sequence.

Русский

Для последовательности f: ℕ → α и сдвига k по нат. числу, limsup сдвинутой последовательности равно limsup исходной.

LaTeX

$$$ \\operatorname{limsup}(f(\\cdot + k)) = \\operatorname{limsup}(f) $$$

Lean4

@[simp]
theorem limsup_nat_add (f : ℕ → α) (k : ℕ) : limsup (fun i => f (i + k)) atTop = limsup f atTop :=
  @liminf_nat_add αᵒᵈ _ f k

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