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 α.