partialSups_eq_sup_range — Mathlib

English

For α with an OrderBot and any f: ℕ → α, the i-th partialSups value is the supremum over the first i+1 values, i.e. (Finset.range(i+1)).sup f.

Русский

Для α с OrderBot и любой функции f: ℕ → α, значение partialSups f на позиции i равно супремуму первых i+1 значений: (Finset.range(i+1)).sup f.

LaTeX

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

Lean4

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

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