Commit 2023-10-11 20:05 7dffcc4b

View on Github →

feat(MeasureTheory/../Prod): drop unneeded assumptions (#7620)

  • Drop CompleteSpace assumption in all theorems about Bochner integral on α × β.
  • Drop measurability assumption in lintegral_prod_swap.

Estimated changes

modified theorem MeasureTheory.integral_prod