English
In a space with HasContDiffBump E, there exists a canonical ContDiffBumpBase E.
Русский
В пространстве с наличием HasContDiffBump E существует каноническая ContDiffBumpBase E.
LaTeX
$$$ \exists b \in ContDiffBumpBase(E). $$$
Lean4
/-- In a space with `C^∞` bump functions, register some function that will be used as a basis
to construct bump functions of arbitrary size around any point. -/
def someContDiffBumpBase (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] [hb : HasContDiffBump E] :
ContDiffBumpBase E :=
Nonempty.some hb.out