iSup_nat_gt_zero_eq — Mathlib

English

For a sequence f: ℕ → α, the supremum over i > 0 equals the supremum over i of f(i+1): ⨆ i>0, f(i) = ⨆ i, f(i+1).

Русский

Для последовательности f: ℕ → α, верхняя грань по i>0 равна верхней грани по i+1: ⨆ i>0 f(i) = ⨆ i f(i+1).

LaTeX

$$$\sup_{i>0} f(i) = \sup_{i} f(i+1)$$$

Lean4

theorem iSup_nat_gt_zero_eq (f : ℕ → α) : ⨆ i > 0, f i = ⨆ i, f (i + 1) :=
  @iInf_nat_gt_zero_eq αᵒᵈ _ f

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