Theorems · Definition · global analysis

SmoothBumpFunction.updateRIn

{E : Type uE} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type uH} →
        [inst_2 : TopologicalSpace H] →
          {I : ModelWithCorners ℝ E H} →
            {M : Type uM} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] →
                  {c : M} → (f : SmoothBumpFunction I c) → (r : ℝ) → r ∈ Set.Ioo 0 f.rOut → SmoothBumpFunction I c

Replace rIn with another value in the interval (0, f.rOut).

Defined in

Mathlib.Geometry.Manifold.BumpFunction

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpace