Documentation

Mathlib.Geometry.Manifold.BumpFunction

Smooth bump functions on a smooth manifold #

In this file we define SmoothBumpFunction I c to be a bundled smooth "bump" function centered at c. It is a structure that consists of two real numbers 0 < rIn < rOut with small enough rOut. We define a coercion to function for this type, and for f : SmoothBumpFunction I c, the function โ‡‘f written in the extended chart at c has the following properties:

The actual statements involve (pre)images under extChartAt I f and are given as lemmas in the SmoothBumpFunction namespace.

Tags #

manifold, smooth bump function

Smooth bump function #

In this section we define a structure for a bundled smooth bump function and prove its properties.

source
๐Ÿ”ถ coverage
structure SmoothBumpFunction {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners โ„ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] (c : M) extends ContDiffBump (โ†‘(extChartAt I c) c) :
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.

Instances For
    source
    ๐Ÿ”ธ coverage
    def SmoothBumpFunction.toFun {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional โ„ E] {c : M} (f : SmoothBumpFunction I c) :
    M โ†’ โ„

    The function defined by f : SmoothBumpFunction c. Use automatic coercion to function instead.

    Equations
      Instances For
        source
        ๐Ÿ”ธ coverage
        instance SmoothBumpFunction.instCoeFunForallReal {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional โ„ E] {c : M} :
        CoeFun (SmoothBumpFunction I c) fun (x : SmoothBumpFunction I c) => M โ†’ โ„
        Equations
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.coe_def {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional โ„ E] {c : M} (f : SmoothBumpFunction I c) :
          โ†‘f = (chartAt H c).source.indicator (โ†‘f.toContDiffBump โˆ˜ โ†‘(extChartAt I c))
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.rOut_pos {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) :
          0 < f.rOut
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.ball_subset {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) :
          Metric.ball (โ†‘(extChartAt I c) c) f.rOut โˆฉ Set.range โ†‘I โŠ† (extChartAt I c).target
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.ball_inter_range_eq_ball_inter_target {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) :
          Metric.ball (โ†‘(extChartAt I c) c) f.rOut โˆฉ Set.range โ†‘I = Metric.ball (โ†‘(extChartAt I c) c) f.rOut โˆฉ (extChartAt I c).target
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.eqOn_source {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] :
          Set.EqOn (โ†‘f) (โ†‘f.toContDiffBump โˆ˜ โ†‘(extChartAt I c)) (chartAt H c).source
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.eventuallyEq_of_mem_source {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {x : M} [FiniteDimensional โ„ E] (hx : x โˆˆ (chartAt H c).source) :
          โ†‘f =แถ [nhds x] โ†‘f.toContDiffBump โˆ˜ โ†‘(extChartAt I c)
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.one_of_dist_le {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {x : M} [FiniteDimensional โ„ E] (hs : x โˆˆ (chartAt H c).source) (hd : dist (โ†‘(extChartAt I c) x) (โ†‘(extChartAt I c) c) โ‰ค f.rIn) :
          โ†‘f x = 1
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.support_eq_inter_preimage {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] :
          Function.support โ†‘f = (chartAt H c).source โˆฉ โ†‘(extChartAt I c) โปยน' Metric.ball (โ†‘(extChartAt I c) c) f.rOut
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.isOpen_support {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] :
          IsOpen (Function.support โ†‘f)
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.support_eq_symm_image {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] :
          Function.support โ†‘f = โ†‘(extChartAt I c).symm '' (Metric.ball (โ†‘(extChartAt I c) c) f.rOut โˆฉ Set.range โ†‘I)
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.support_subset_source {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] :
          Function.support โ†‘f โŠ† (chartAt H c).source
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.image_eq_inter_preimage_of_subset_support {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] {s : Set M} (hs : s โŠ† Function.support โ†‘f) :
          โ†‘(extChartAt I c) '' s = Metric.closedBall (โ†‘(extChartAt I c) c) f.rOut โˆฉ Set.range โ†‘I โˆฉ โ†‘(extChartAt I c).symm โปยน' s
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.mem_Icc {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {x : M} [FiniteDimensional โ„ E] :
          โ†‘f x โˆˆ Set.Icc 0 1
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.nonneg {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {x : M} [FiniteDimensional โ„ E] :
          0 โ‰ค โ†‘f x
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.le_one {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {x : M} [FiniteDimensional โ„ E] :
          โ†‘f x โ‰ค 1
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.eventuallyEq_one_of_dist_lt {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {x : M} [FiniteDimensional โ„ E] (hs : x โˆˆ (chartAt H c).source) (hd : dist (โ†‘(extChartAt I c) x) (โ†‘(extChartAt I c) c) < f.rIn) :
          โ†‘f =แถ [nhds x] 1
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.eventuallyEq_one {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] :
          โ†‘f =แถ [nhds c] 1
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem SmoothBumpFunction.eq_one {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] :
          โ†‘f c = 1
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.support_mem_nhds {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] :
          Function.support โ†‘f โˆˆ nhds c
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.tsupport_mem_nhds {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] :
          tsupport โ†‘f โˆˆ nhds c
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.c_mem_support {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] :
          c โˆˆ Function.support โ†‘f
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.nonempty_support {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] :
          (Function.support โ†‘f).Nonempty
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.isCompact_symm_image_closedBall {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] :
          IsCompact (โ†‘(extChartAt I c).symm '' (Metric.closedBall (โ†‘(extChartAt I c) c) f.rOut โˆฉ Set.range โ†‘I))
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.nhdsWithin_range_basis {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} :
          (nhdsWithin (โ†‘(extChartAt I c) c) (Set.range โ†‘I)).HasBasis (fun (x : SmoothBumpFunction I c) => True) fun (f : SmoothBumpFunction I c) => Metric.closedBall (โ†‘(extChartAt I c) c) f.rOut โˆฉ Set.range โ†‘I

          Given a smooth bump function f : SmoothBumpFunction I c, the closed ball of radius f.R is known to include the support of f. These closed balls (in the model normed space E) intersected with Set.range I form a basis of ๐“[range I] (extChartAt I c c).

          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.isClosed_image_of_isClosed {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] {s : Set M} (hsc : IsClosed s) (hs : s โŠ† Function.support โ†‘f) :
          IsClosed (โ†‘(extChartAt I c) '' s)
          source
          ๐Ÿ“ coverage
          theorem SmoothBumpFunction.exists_r_pos_lt_subset_ball {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] {s : Set M} (hsc : IsClosed s) (hs : s โŠ† Function.support โ†‘f) :
          โˆƒ r โˆˆ Set.Ioo 0 f.rOut, s โŠ† (chartAt H c).source โˆฉ โ†‘(extChartAt I c) โปยน' Metric.ball (โ†‘(extChartAt I c) c) r

          If f is a smooth bump function and s closed subset of the support of f (i.e., of the open ball of radius f.rOut), then there exists 0 < r < f.rOut such that s is a subset of the open ball of radius r. Formally, s โŠ† e.source โˆฉ e โปยน' (ball (e c) r), where e = extChartAt I c.

          source
          ๐Ÿ”ธ coverage
          def SmoothBumpFunction.updateRIn {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) (r : โ„) (hr : r โˆˆ Set.Ioo 0 f.rOut) :
          SmoothBumpFunction I c

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

          Equations
            Instances For
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem SmoothBumpFunction.updateRIn_rIn {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) (r : โ„) (hr : r โˆˆ Set.Ioo 0 f.rOut) :
              (f.updateRIn r hr).rIn = r
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem SmoothBumpFunction.updateRIn_rOut {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) (r : โ„) (hr : r โˆˆ Set.Ioo 0 f.rOut) :
              (f.updateRIn r hr).rOut = f.rOut
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem SmoothBumpFunction.support_updateRIn {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] {r : โ„} (hr : r โˆˆ Set.Ioo 0 f.rOut) :
              Function.support โ†‘(f.updateRIn r hr) = Function.support โ†‘f
              source
              ๐Ÿ“ coverage
              instance SmoothBumpFunction.instNonempty {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} :
              Nonempty (SmoothBumpFunction I c)
              source
              ๐Ÿ“ coverage
              theorem SmoothBumpFunction.isClosed_symm_image_closedBall {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] [T2Space M] :
              IsClosed (โ†‘(extChartAt I c).symm '' (Metric.closedBall (โ†‘(extChartAt I c) c) f.rOut โˆฉ Set.range โ†‘I))
              source
              ๐Ÿ“ coverage
              theorem SmoothBumpFunction.tsupport_subset_symm_image_closedBall {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] [T2Space M] :
              tsupport โ†‘f โŠ† โ†‘(extChartAt I c).symm '' (Metric.closedBall (โ†‘(extChartAt I c) c) f.rOut โˆฉ Set.range โ†‘I)
              source
              ๐Ÿ“ coverage
              theorem SmoothBumpFunction.tsupport_subset_extChartAt_source {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] [T2Space M] :
              tsupport โ†‘f โŠ† (extChartAt I c).source
              source
              ๐Ÿ“ coverage
              theorem SmoothBumpFunction.tsupport_subset_chartAt_source {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] [T2Space M] :
              tsupport โ†‘f โŠ† (chartAt H c).source
              source
              ๐Ÿ“ coverage
              theorem SmoothBumpFunction.hasCompactSupport {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] [T2Space M] :
              HasCompactSupport โ†‘f
              source
              ๐Ÿ“ coverage
              theorem SmoothBumpFunction.nhds_basis_tsupport {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] (c : M) [FiniteDimensional โ„ E] [T2Space M] :
              (nhds c).HasBasis (fun (x : SmoothBumpFunction I c) => True) fun (f : SmoothBumpFunction I c) => tsupport โ†‘f

              The closures of supports of smooth bump functions centered at c form a basis of ๐“ c. In other words, each of these closures is a neighborhood of c and each neighborhood of c includes tsupport f for some f : SmoothBumpFunction I c.

              source
              ๐Ÿ“ coverage
              theorem SmoothBumpFunction.nhds_basis_support {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} [FiniteDimensional โ„ E] [T2Space M] {s : Set M} (hs : s โˆˆ nhds c) :
              (nhds c).HasBasis (fun (f : SmoothBumpFunction I c) => tsupport โ†‘f โŠ† s) fun (f : SmoothBumpFunction I c) => Function.support โ†‘f

              Given s โˆˆ ๐“ c, the supports of smooth bump functions f : SmoothBumpFunction I c such that tsupport f โŠ† s form a basis of ๐“ c. In other words, each of these supports is a neighborhood of c and each neighborhood of c includes support f for some f : SmoothBumpFunction I c such that tsupport f โŠ† s.

              source
              ๐Ÿ“ coverage
              theorem SmoothBumpFunction.contMDiff {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] [T2Space M] [IsManifold I (โ†‘โŠค) M] :
              ContMDiff I (modelWithCornersSelf โ„ โ„) โ†‘โŠค โ†‘f

              A smooth bump function is infinitely smooth.

              source
              ๐Ÿ“ coverage
              theorem SmoothBumpFunction.contMDiffAt {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] [T2Space M] [IsManifold I (โ†‘โŠค) M] {x : M} :
              ContMDiffAt I (modelWithCornersSelf โ„ โ„) (โ†‘โŠค) (โ†‘f) x
              source
              ๐Ÿ“ coverage
              theorem SmoothBumpFunction.continuous {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] [T2Space M] [IsManifold I (โ†‘โŠค) M] :
              Continuous โ†‘f
              source
              ๐Ÿ“ coverage
              theorem SmoothBumpFunction.contMDiff_smul {E : Type uE} [NormedAddCommGroup E] [NormedSpace โ„ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners โ„ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional โ„ E] [T2Space M] [IsManifold I (โ†‘โŠค) M] {G : Type u_1} [NormedAddCommGroup G] [NormedSpace โ„ G] {g : M โ†’ G} (hg : ContMDiffOn I (modelWithCornersSelf โ„ G) (โ†‘โŠค) g (chartAt H c).source) :
              ContMDiff I (modelWithCornersSelf โ„ G) โ†‘โŠค fun (x : M) => โ†‘f x โ€ข g x

              If f : SmoothBumpFunction I c is a smooth bump function and g : M โ†’ G is a function smooth on the source of the chart at c, then f โ€ข g is smooth on the whole manifold.