Commit 2023-06-07 00:58 b90d4a04

View on Github →

feat: port MeasureTheory.Function.ContinuousMapDense (#4760)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

added theorem BoundedContinuousFunction.toLp_denseRange

added theorem ContinuousMap.toLp_denseRange

added theorem MeasureTheory.Integrable.exists_boundedContinuous_integral_sub_le

added theorem MeasureTheory.Integrable.exists_boundedContinuous_lintegral_sub_le

added theorem MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le

added theorem MeasureTheory.Integrable.exists_hasCompactSupport_lintegral_sub_le

added theorem MeasureTheory.Lp.boundedContinuousFunction_dense

added theorem MeasureTheory.Memℒp.exists_boundedContinuous_integral_rpow_sub_le

added theorem MeasureTheory.Memℒp.exists_boundedContinuous_snorm_sub_le

added theorem MeasureTheory.Memℒp.exists_hasCompactSupport_integral_rpow_sub_le

added theorem MeasureTheory.Memℒp.exists_hasCompactSupport_snorm_sub_le

added theorem MeasureTheory.exists_continuous_snorm_sub_le_of_closed