Theorems · Definition · global analysis

ExistsContDiffBumpBase.w

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] → [FiniteDimensional ℝ E] → [inst_3 : MeasurableSpace E] → [BorelSpace E] → ℝ → E → ℝ

An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces, which is smooth, symmetric, with support equal to the ball of radius D and integral 1.

Defined in

Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Cited by

11 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpace