α : Type u_1
β : Type ?u.580401
ι : Type ?u.580404
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ ‖f n‖ ≤ C * r ^ n
α : Type u_1
β : Type ?u.580401
ι : Type ?u.580404
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ dist (∑ i in Finset.range n, f i) (∑ i in Finset.range (n + 1), f i) ≤ C * r ^ n
rw [sum_range_succ, dist_eq_norm, ← norm_neg, neg_sub, add_sub_cancel']
no goals
α : Type u_1
β : Type ?u.580401
ι : Type ?u.580404
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ ‖f n‖ ≤ C * r ^ n
exact hf n