Theorems · Inductive type · global analysis

SmoothBumpFunction

{E : Type uE} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type uH} →
        [inst_2 : TopologicalSpace H] →
          ModelWithCorners ℝ E H → {M : Type uM} → [inst : TopologicalSpace M] → [ChartedSpace H M] → M → Type

Given a smooth manifold modelled on a finite-dimensional space E, f : SmoothBumpFunction I M is a smooth function on M such that in the extended chart e at f.c: * f x = 1 in the closed ball of radius f.rIn centered at f.c; * f x = 0 outside of the ball of radius f.rOut centered at f.c; * 0 ≤ f x ≤ 1 for all x. The structure contains data required to construct a function with these properties. The function is available as ⇑f or f x. Formal statements of the properties listed above involve some (pre)images under extChartAt I f.c and are given as lemmas in the SmoothBumpFunction namespace.

Defined in

Mathlib.Geometry.Manifold.BumpFunction

Cited by

50 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpace