Theorem MeasureTheory.integral_integral_swap_of_hasCompactSupport

Modification history

2023-11-03 14:28
Mathlib/MeasureTheory/Constructions/Prod/Integral.lean
feat: Fubini for functions with compact support and non-sigma-finite measures (#8125)
Added MeasureTheory.integral_integral_swap_of_hasCompactSupportView on Github →