The existence of smooth bumps, separated from their construction.
theorem
FiniteDimensional.hasContDiffBump
(E : Type u_1)
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
:
A finite-dimensional real normed space admits smooth bump functions. This proof can be activated as an instance locally when defining cutoff data.