α : Type u_1
f : α → ℝ≥0
⊢ Tendsto (fun a => ∑' (a_1 : { x // ¬x ∈ a }), ↑(f ↑a_1)) atTop (𝓝 0)
α : Type u_1
f : α → ℝ≥0
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop (𝓝 0)
simp_rw [← tendsto_coe, coe_tsum, NNReal.coe_zero]
no goals
α : Type u_1
f : α → ℝ≥0
⊢ Tendsto (fun a => ∑' (a_1 : { x // ¬x ∈ a }), ↑(f ↑a_1)) atTop (𝓝 0)
exact tendsto_tsum_compl_atTop_zero fun a : α => (f a : ℝ)