Theorem MeasureTheory.integral_union_ae

Modification history

2026-03-05 01:06
Mathlib/MeasureTheory/Integral/Bochner/Set.lean
feat(Integral.Bochner.Set): add `tendsto_setIntegral_of_monotone₀` (#34025) …
Deleted MeasureTheory.integral_union_aeView on Github →
2025-04-15 08:42
Mathlib/MeasureTheory/Integral/Bochner/Set.lean
chore: split `MeasureTheory.Integral.SetIntegral` (#24070) …
Modified MeasureTheory.integral_union_aeView on Github →
2023-06-06 00:38
Mathlib/MeasureTheory/Integral/SetIntegral.lean
feat: port MeasureTheory.Integral.SetIntegral (#4690)
Added MeasureTheory.integral_union_aeView on Github →