Commit 2026-06-25 13:57 aea5d67c

View on Github →

chore(MeasureTheory): minor clean up of seminorm lemmas (#40986) Remove a duplicate lemma and generalize some lemmas to support two different codomains.

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

modified theorem MeasureTheory.eLpNorm'_congr_enorm_ae

modified theorem MeasureTheory.eLpNorm'_congr_nnnorm_ae

modified theorem MeasureTheory.eLpNorm'_congr_norm_ae

modified theorem MeasureTheory.eLpNormEssSup_mono_enorm_ae

modified theorem MeasureTheory.eLpNormEssSup_mono_nnnorm_ae

deleted theorem MeasureTheory.eLpNorm_mono_ae'

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Indicator.lean