Commit 2026-01-26 14:38 35578db0

View on Github →

chore(L1Space/HasFiniteIntegral): rename three lemmas (#34439) Discovered in #24343.

Estimated changes

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

added theorem MeasureTheory.ae_norm_ofReal_f_le_bound

added theorem MeasureTheory.ae_tendsto_ofReal_norm

added theorem MeasureTheory.all_ae_norm_ofReal_F_le_bound

deleted theorem MeasureTheory.all_ae_ofReal_F_le_bound

deleted theorem MeasureTheory.all_ae_ofReal_f_le_bound

deleted theorem MeasureTheory.all_ae_tendsto_ofReal_norm