case intro
α : Type u_1
β : Type ?u.307697
γ : Type ?u.307700
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f : α → ℝ≥0
hsum : (∑' (x : α), (fun i => ↑(f i)) x) ≠ ⊤
⊢ HasSum (fun x => ENNReal.toReal ((fun i => ↑(f i)) x)) (∑' (x : α), ENNReal.toReal ((fun i => ↑(f i)) x))
α : Type u_1
β : Type ?u.307697
γ : Type ?u.307700
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f : α → ℝ≥0∞
hsum : (∑' (x : α), f x) ≠ ⊤
⊢ HasSum (fun x => ENNReal.toReal (f x)) (∑' (x : α), ENNReal.toReal (f x))
lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hsum
case intro
α : Type u_1
β : Type ?u.307697
γ : Type ?u.307700
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f : α → ℝ≥0
hsum : (∑' (x : α), (fun i => ↑(f i)) x) ≠ ⊤
⊢ HasSum (fun a => f a) (∑' (a : α), f a)
case intro
α : Type u_1
β : Type ?u.307697
γ : Type ?u.307700
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f : α → ℝ≥0
hsum : (∑' (x : α), (fun i => ↑(f i)) x) ≠ ⊤
⊢ HasSum (fun x => ENNReal.toReal ((fun i => ↑(f i)) x)) (∑' (x : α), ENNReal.toReal ((fun i => ↑(f i)) x))
simp only [coe_toReal, ← NNReal.coe_tsum, NNReal.hasSum_coe]
no goals
case intro
α : Type u_1
β : Type ?u.307697
γ : Type ?u.307700
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f : α → ℝ≥0
hsum : (∑' (x : α), (fun i => ↑(f i)) x) ≠ ⊤
⊢ HasSum (fun a => f a) (∑' (a : α), f a)
exact (tsum_coe_ne_top_iff_summable.1 hsum).hasSum