Commit 2024-08-09 14:31 c0ec0639
View on Github →feat: add lemma relating Set.encard to tsum over ennreal (#15214)
two lemmas: s.tsum (1:ENNReal) = s.encard
and s.tsum c = s.encard * c
, where c:ENNReal
and s : Set α
.
feat: add lemma relating Set.encard to tsum over ennreal (#15214)
two lemmas: s.tsum (1:ENNReal) = s.encard
and s.tsum c = s.encard * c
, where c:ENNReal
and s : Set α
.