α : Type ?u.1626294
β : Type ?u.1626297
ι : Type ?u.1626300
E : Type ?u.1626303
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
n : ℕ
⊢ ‖if Even n then 0 else 1‖ ≤ 1
α : Type ?u.1626294
β : Type ?u.1626297
ι : Type ?u.1626300
E : Type ?u.1626303
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
n : ℕ
⊢ ‖∑ i in Finset.range n, (-1) ^ i‖ ≤ 1
rw [neg_one_geom_sum]
no goals
α : Type ?u.1626294
β : Type ?u.1626297
ι : Type ?u.1626300
E : Type ?u.1626303
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
n : ℕ
⊢ ‖if Even n then 0 else 1‖ ≤ 1
split_ifs <;> norm_num