someContDiffBumpBase — Mathlib

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

Похожие утверждения