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

Estimated changes