Theorem MeasureTheory.norm_setIntegral_le_of_norm_le_const'

Modification history

2025-04-19 15:05

Mathlib/MeasureTheory/Integral/Bochner/Set.lean

feat: drop measurability assumption in `norm_setIntegral_le_of_norm_le_const_ae'` (#24134)

Deleted MeasureTheory.norm_setIntegral_le_of_norm_le_const'View on Github →

2025-04-15 08:42

Mathlib/MeasureTheory/Integral/Bochner/Set.lean

chore: split `MeasureTheory.Integral.SetIntegral` (#24070) …

Modified MeasureTheory.norm_setIntegral_le_of_norm_le_const'View on Github →

2024-04-18 02:39

Mathlib/MeasureTheory/Integral/SetIntegral.lean

chore: replace `set_integral` with `setIntegral` (#12215) …

Added MeasureTheory.norm_setIntegral_le_of_norm_le_const'View on Github →