case intro
α : Type ?u.343727
β : Type ?u.343730
γ : Type ?u.343733
f : ℕ → ℝ≥0
⊢ (¬Summable fun i => ↑(f i)) ↔ Tendsto (fun n => ∑ i in Finset.range n, (fun i => ↑(f i)) i) atTop atTop
α : Type ?u.343727
β : Type ?u.343730
γ : Type ?u.343733
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ ¬Summable f ↔ Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
lift f to ℕ → ℝ≥0 using hf
no goals
case intro
α : Type ?u.343727
β : Type ?u.343730
γ : Type ?u.343733
f : ℕ → ℝ≥0
⊢ (¬Summable fun i => ↑(f i)) ↔ Tendsto (fun n => ∑ i in Finset.range n, (fun i => ↑(f i)) i) atTop atTop
exact_mod_cast NNReal.not_summable_iff_tendsto_nat_atTop