Infinite sums of ENNReal and Set.encard

This file provides lemmas relating sums of constants to the cardinality of the domain of these sums.

TODO

• Once we have a topology on ENat, provide an ENat valued version
• Once we replace PartENat entirely with ENat (and replace PartENat.card with a ENat.card), provide versions which sum over the whole type.

@[simp]

theorem ENNReal.tsum_set_one_eq {α : Type u_1} (s : Set α) : ∑' (x : ↑s), 1 = ↑s.encard

@[simp]

theorem ENNReal.tsum_set_const_eq {α : Type u_1} (s : Set α) (c : ENNReal) : ∑' (x : ↑s), c = ↑s.encard * c