Commit 2026-02-04 08:12 73b87014

View on Github →

feat: use HasSolidNorm in Integrable.measure_ge_lt_top (#34769)

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

modified theorem MeasureTheory.Integrable.measure_ge_lt_top

modified theorem MeasureTheory.Integrable.measure_gt_lt_top

modified theorem MeasureTheory.Integrable.measure_le_lt_top

modified theorem MeasureTheory.Integrable.measure_lt_lt_top