Commit 2024-07-09 23:50 e242f1ed

View on Github →

feat: add denseRange_subtype_val (#14592) Also add MeasureTheory.Lp.simpleFunc.dense

Estimated changes

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/Topology/Basic.lean

modified theorem Dense.denseRange_val

added theorem denseRange_subtype_val