A question about ENNReal

Stream: new members

[Ching-Tsun Chou]

Under the assumption that:

variable (ι : Type*) (s : Set ι) (h : s.Infinite) (c : ENNReal)

how does one go about proving that the following sum:

∑' (_ : ↑s), c

is either 0 or infinity depending on whether c is 0 or positive?

[Matt Diamond]

docs#ENNReal.tsum_const_eq_top_of_ne_zero should be useful here (along with docs#tsum_zero)

[Matt Diamond]

import Mathlib

variable (ι : Type*) (s : Set ι) (h : s.Infinite) (c : ENNReal)

example (hc : c = 0) : ∑' (_ : ↑s), c = 0 := by rw [hc, tsum_zero]

example (hc : c ≠ 0) : ∑' (_ : ↑s), c = ⊤ :=
have : Infinite ↑s := h.to_subtype
ENNReal.tsum_const_eq_top_of_ne_zero hc

[Ching-Tsun Chou]

Thanks! That's exactly what I need.