iInf_iSup_ge_nat_add — Mathlib

English

For a sequence f: ℕ → α and k ∈ ℕ, the dual of the previous shift identity holds: iInf of iSup of iInf with f(i+k) equals iInf of iSup of iInf with f(i).

Русский

Для последовательности f: ℕ → α и k ∈ ℕ справедливо двойное преобразование сдвига в двойной форме: iInf iSup iInf с f(i+k) равно iInf iSup iInf с f(i).

LaTeX

$$$\displaystyle \text{(dual shift identity)}$$$

Lean4

theorem iInf_iSup_ge_nat_add : ∀ (f : ℕ → α) (k : ℕ), ⨅ n, ⨆ i ≥ n, f (i + k) = ⨅ n, ⨆ i ≥ n, f i :=
  @iSup_iInf_ge_nat_add αᵒᵈ _

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