Commit 2023-05-21 16:45 76bc1654

View on Github →

feat: port MeasureTheory.Function.SimpleFuncDense (#4099)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/SimpleFuncDense.lean

added theorem MeasureTheory.SimpleFunc.approxOn_comp

added theorem MeasureTheory.SimpleFunc.approxOn_mem

added theorem MeasureTheory.SimpleFunc.approxOn_zero

added theorem MeasureTheory.SimpleFunc.edist_approxOn_le

added theorem MeasureTheory.SimpleFunc.edist_approxOn_mono

added theorem MeasureTheory.SimpleFunc.edist_approxOn_y0_le

added theorem MeasureTheory.SimpleFunc.edist_nearestPt_le

added theorem MeasureTheory.SimpleFunc.nearestPtInd_le

added theorem MeasureTheory.SimpleFunc.nearestPtInd_succ

added theorem MeasureTheory.SimpleFunc.nearestPtInd_zero

added theorem MeasureTheory.SimpleFunc.nearestPt_zero

added theorem MeasureTheory.SimpleFunc.tendsto_approxOn

added theorem MeasureTheory.SimpleFunc.tendsto_nearestPt