Theorem Continuous.exists_contDiff_approx_and_eqOn

Modification history

2025-11-17 21:06
Mathlib/Geometry/Manifold/SmoothApprox.lean
feat: approximate continuous functions by smooth functions (#31278) …
Added Continuous.exists_contDiff_approx_and_eqOnView on Github →