partialSups_eq_sup'_range — Mathlib

English

For f: ℕ → α and n ∈ ℕ, partialSups f n equals the supremum over the first n+1 indices: (Finset.range(n+1)).sup' nonempty_range_add_one f.

Русский

Для функции f: ℕ → α и натурального n, partialSups f n есть верхняя грань по первому диапазону из n+1 элементов: (Finset.range(n+1)).sup' nonempty_range_add_one f.

LaTeX

$$$\\mathrm{partialSups} f\, n \;=\\; (\\mathrm{Finset.range}(n+1)).\\mathrm{sup}'\\, f$$$

Lean4

theorem partialSups_eq_sup'_range (f : ℕ → α) (n : ℕ) :
    partialSups f n = (Finset.range (n + 1)).sup' nonempty_range_add_one f :=
  eq_of_forall_ge_iff fun _ ↦ by simp [Nat.lt_succ_iff]

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