ι : Type u_2
κ : Type ?u.47829
α : Type u_1
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hsum : Summable g
hg : ∀ (i : ι), 0 ≤ g i
i : ι
hi : 0 < g i
⊢ (∑' (x : ?m.49191), 0) < ∑' (i : ι), g i

ι : Type u_2
κ : Type ?u.47829
α : Type u_1
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hsum : Summable g
hg : ∀ (i : ι), 0 ≤ g i
i : ι
hi : 0 < g i
⊢ Type ?u.49189
ι : Type u_2
κ : Type ?u.47829
α : Type u_1
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hsum : Summable g
hg : ∀ (i : ι), 0 ≤ g i
i : ι
hi : 0 < g i
⊢ 0 < ∑' (i : ι), g i
rw [← tsum_zero]
no goals
ι : Type u_2
κ : Type ?u.47829
α : Type u_1
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hsum : Summable g
hg : ∀ (i : ι), 0 ≤ g i
i : ι
hi : 0 < g i
⊢ (∑' (x : ?m.49191), 0) < ∑' (i : ι), g i

ι : Type u_2
κ : Type ?u.47829
α : Type u_1
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hsum : Summable g
hg : ∀ (i : ι), 0 ≤ g i
i : ι
hi : 0 < g i
⊢ Type ?u.49189
exact tsum_lt_tsum hg hi summable_zero hsum