no goals
α : Type ?u.345613
β : Type ?u.345616
γ : Type ?u.345619
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable f ↔ ¬Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop_of_nonneg hf]