iSup_nat_add — Mathlib

English

If f: ℕ → α is monotone and k ∈ ℕ, then shifting the index by k does not change the supremum: ⨆ n, f(n+k) = ⨆ n, f(n).

Русский

Если f: ℕ → α монотонна и k ∈ ℕ, то сдвиг индекса на k не меняет верхнюю грань: ⨆ n, f(n+k) = ⨆ n, f(n).

LaTeX

$$$\displaystyle \big\langle \sup_{n} f(n+k) = \sup_{n} f(n) \rangle$$$

Lean4

theorem iSup_nat_add {f : ℕ → α} (hf : Monotone f) (k : ℕ) : ⨆ n, f (n + k) = ⨆ n, f n :=
  le_antisymm (iSup_le fun i => le_iSup _ (i + k)) <| iSup_mono fun i => hf <| Nat.le_add_right i k

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