α : Type ?u.312215
β : Type ?u.312218
γ : Type ?u.312221
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ Tendsto (fun n => ∑ i in Finset.range n, ↑(f i)) atTop (𝓝 ↑r) ↔
    Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 r)
α : Type ?u.312215
β : Type ?u.312218
γ : Type ?u.312221
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ HasSum f r ↔ Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 r)
rw [← ENNReal.hasSum_coe, ENNReal.hasSum_iff_tendsto_nat]
α : Type ?u.312215
β : Type ?u.312218
γ : Type ?u.312221
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ Tendsto (fun n => ↑(∑ a in Finset.range n, f a)) atTop (𝓝 ↑r) ↔
    Tendsto (fun n => ∑ a in Finset.range n, f a) atTop (𝓝 r)
α : Type ?u.312215
β : Type ?u.312218
γ : Type ?u.312221
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ Tendsto (fun n => ∑ i in Finset.range n, ↑(f i)) atTop (𝓝 ↑r) ↔
    Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 r)
simp only [← ENNReal.coe_finset_sum]
no goals
α : Type ?u.312215
β : Type ?u.312218
γ : Type ?u.312221
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ Tendsto (fun n => ↑(∑ a in Finset.range n, f a)) atTop (𝓝 ↑r) ↔
    Tendsto (fun n => ∑ a in Finset.range n, f a) atTop (𝓝 r)
exact ENNReal.tendsto_coe