case pos
ι : Type u_2
κ : Type ?u.33257
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), f i ≤ 0
hf : Summable f
⊢ (∑' (i : ι), f i) ≤ 0

case neg
ι : Type u_2
κ : Type ?u.33257
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), f i ≤ 0
hf : ¬Summable f
⊢ (∑' (i : ι), f i) ≤ 0
ι : Type u_2
κ : Type ?u.33257
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), f i ≤ 0
⊢ (∑' (i : ι), f i) ≤ 0
by_cases hf : Summable f
no goals
case pos
ι : Type u_2
κ : Type ?u.33257
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), f i ≤ 0
hf : Summable f
⊢ (∑' (i : ι), f i) ≤ 0
exact hf.hasSum.nonpos h
no goals
case neg
ι : Type u_2
κ : Type ?u.33257
α : Type u_1
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), f i ≤ 0
hf : ¬Summable f
⊢ (∑' (i : ι), f i) ≤ 0
rw [tsum_eq_zero_of_not_summable hf]