dist_partial_sum' — Mathlib

English

For any α in a seminormed additive group and any sequence u: N → α, the distance between the first n partial sums and the first n+1 partial sums is ∥u(n)∥.

Русский

Для любой последовательности u: N → α в семинормированной аддитивной группе расстояние между суммами первых n и первых n+1 членов равно ∥u(n)∥.

LaTeX

$$$\forall {\alpha} [\text{SeminormedAddCommGroup } \alpha] (u : \mathbb{N} \to \alpha) (n : \mathbb{N}), \; dist\Big(\sum_{k< n} u(k), \sum_{k< (n+1)} u(k)\Big) = \|u(n)\|$$$

Lean4

@[simp]
theorem dist_partial_sum' (u : ℕ → α) (n : ℕ) : dist (∑ k ∈ range n, u k) (∑ k ∈ range (n + 1), u k) = ‖u n‖ := by
  simp [dist_eq_norm', sum_range_succ]

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