sum_tsub_distrib — Mathlib

English

In a monotone setting, the sum from 0 to n-1 of (f(i+1) - f(i)) equals f(n) - f(0).

Русский

В предположении монотонности сумма от 0 до n-1 (f(i+1) - f(i)) равна f(n) - f(0).

LaTeX

$$$$ \\sum_{i=0}^{n-1} (f(i+1) - f(i)) = f(n) - f(0) $$$$

Lean4

theorem sum_tsub_distrib (s : Finset ι) {f g : ι → M} (hfg : ∀ x ∈ s, g x ≤ f x) :
    ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x :=
  Multiset.sum_map_tsub _ hfg

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