liminf_nat_add — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem liminf_nat_add (f : ℕ → α) (k : ℕ) : liminf (fun i => f (i + k)) atTop = liminf f atTop := by
  rw [← Function.comp_def, liminf, liminf, ← map_map, map_add_atTop_eq_nat]

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