Commit 2024-07-15 20:56 60a7755e

View on Github →

feat(Function/LpSpace): continuity of indicatorConstLp in the set (#14489)

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

added theorem MeasureTheory.Lp.indicatorConstLp_compMeasurePreserving

added theorem MeasureTheory.Lp.toLp_compMeasurePreserving

added theorem MeasureTheory.Memℒp.toLp_val

added theorem MeasureTheory.continuous_indicatorConstLp_set

added theorem MeasureTheory.ennnorm_indicatorConstLp_le

added theorem MeasureTheory.nnnorm_indicatorConstLp_le

added theorem MeasureTheory.tendsto_indicatorConstLp_set