Commit 2023-10-09 06:37 02472004
View on Github →chore(MeasureTheory/../Prod/Integral): Drop an assumption, golf (#7579)
Drop some measurability assumptions by using the fact that Prod.swap
is a measurable equivalence.
chore(MeasureTheory/../Prod/Integral): Drop an assumption, golf (#7579)
Drop some measurability assumptions by using the fact that Prod.swap
is a measurable equivalence.