iInf_nat_add — Mathlib

English

If f: ℕ → α is antitone and k ∈ ℕ, then shifting the index by k preserves the infimum: ⨅ n, f(n+k) = ⨅ n, f(n).

Русский

Если f: ℕ → α антиизотропна, и k ∈ ℕ, то сдвиг индекса на k сохраняет инфиминум: ⨅ n, f(n+k) = ⨅ n, f(n).

LaTeX

$$$\inf_{n} f(n+k) = \inf_{n} f(n)$$$

Lean4

theorem iInf_nat_add {f : ℕ → α} (hf : Antitone f) (k : ℕ) : ⨅ n, f (n + k) = ⨅ n, f n :=
  hf.dual_right.iSup_nat_add k

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