Commit 2022-11-03 18:22 a0381d50

feat(measure_theory/measure/measure_space): Add parallel set of lemmas about count (#17245) This PR adds a parallel set of basic lemmas about measure_theory.measure.count, which does not assume [measurable_singleton_class _] but instead assumes (measurable set _). The same lemmas are true without the [measurable_singleton_class _] assumption, so it often seems inappropriate to require this type class. However, the versions with (measurable_set _) assumption are also not strictly generalizations of the ones with the type class, so the PR adds a parallel set of lemmas (many but not all of the existing proofs reduce to the new lemmas at least partially). The new lemma names are a prime appended to the original lemma names; under the common [measurable_singleton_class _] assumption for counting measures, the original set of lemmas is more convenient. One setup where it is, however, appropriate to relax the [measurable_singleton_class _] assumption is conditional expected values in finite probability spaces with uniform distribution