English
For any α in a seminormed additive group and any sequence u: N → α, the distance between consecutive partial sums equals the norm of the next term: dist(∑_{k=0}^{n} u(k), ∑_{k=0}^{n-1} u(k)) = ∥u(n)∥.
Русский
Для любой α в полугруппе с нормой и любой последовательности u: N → α расстояние между соседними частичными суммами равно норме очередного элемента: dist(∑_{k=0}^{n} u(k), ∑_{k=0}^{n-1} u(k)) = ∥u(n)∥.
LaTeX
$$$\forall {\alpha} [\text{SeminormedAddCommGroup } \alpha] (u : \mathbb{N} \to \alpha) (n : \mathbb{N}), \\ dist\Big(\sum_{k=0}^{n} u(k), \sum_{k=0}^{n-1} u(k)\Big) = \|u(n)\|$$$
Lean4
@[simp]
theorem dist_partial_sum (u : ℕ → α) (n : ℕ) : dist (∑ k ∈ range (n + 1), u k) (∑ k ∈ range n, u k) = ‖u n‖ := by
simp [dist_eq_norm, sum_range_succ]
