Theorems · Inductive type · global analysis

HasContDiffBump

(E : Type u_3) → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → Prop

A class registering that a real vector space admits bump functions. This will be instantiated first for inner product spaces, and then for finite-dimensional normed spaces. We use a specific class instead of Nonempty (ContDiffBumpBase E) for performance reasons.

Defined in

Mathlib.Analysis.Calculus.BumpFunction.Basic

Cited by

46 results in Mathlib

Foundations

Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace