Theorems · Theorem · global analysis

exists_contDiff_tsupport_subset

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E}
  {n : ℕ∞},
  s ∈ nhds x → ∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n) f ∧ Set.range f ⊆ Set.Icc 0 1 ∧ f x = 1

If a set s is a neighborhood of x, then there exists a smooth function f taking values in [0, 1], supported in s and with f x = 1.

Defined in

Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensional