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
    noncomputable 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.

    Instances For
      source
      ๐Ÿ”ธ coverage
      @[implicit_reducible]
      noncomputable 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 โ†’ โ„
      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).

      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.