Commit 2025-08-04 15:00 9a749a69

View on Github →

fix: cleanup measurability + prod/sum lemmas + fun_prop (#25254)

  • Add fun_prop to a few more lemmas
  • Rename the compositional version to something without a prime, add the compositional version for StronglyMeasurable
  • use the prod/fun_prod naming scheme (the compositional version is called prod_apply) for [AE][Strongly]Measurable

Estimated changes

deleted theorem Finset.aemeasurable_prod'
deleted theorem Finset.measurable_prod'
deleted theorem List.aemeasurable_prod'
deleted theorem List.measurable_prod'
modified theorem Multiset.aemeasurable_prod
deleted theorem Multiset.measurable_prod'
modified theorem Multiset.measurable_prod
added theorem measurable_fun_prod
added theorem measurable_fun_sum
deleted theorem measurable_prod
deleted theorem measurable_sum