mathlib
0508c7b1 - feat(analysis/specific_limits): add `set.countable.exists_pos_has_sum_le` (#9052)

Commit

4 years ago

feat(analysis/specific_limits): add `set.countable.exists_pos_has_sum_le` (#9052) Add versions of `pos_sum_of_encodable` for countable sets.

Author

urkud

Parents