Commit 2025-04-22 14:20 be7e73ef

View on Github →

feat(Calculus/BumpFunction/SmoothApprox): new file (#24162) Reformulate theorems about density of smooth functions without measures.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/BumpFunction/SmoothApprox.lean

added theorem Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le

added theorem ContinuousMap.dense_setOf_contDiff

added theorem MeasureTheory.LocallyIntegrable.exists_contDiff_dist_le_of_forall_mem_ball_dist_le

added theorem UniformContinuous.exists_contDiff_dist_le