mathlib3

a0381d50 - feat(measure_theory/measure/measure_space): Add parallel set of lemmas about count (#17245)

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 Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com> Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>