English
If a set s is a neighborhood of x in a finite-dimensional normed space, there exists a smooth function u with compact support inside s, taking values in [0,1], with u(x)=1.
Русский
Если s — окрестность точки x в конечномерном пространстве, то существует гладкая функция u с компактной поддержкой внутри s, значениями в [0,1], и u(x)=1.
LaTeX
$$$\\forall s, x, s\\in 𝓝 x \\Rightarrow \\exists u: E→ℝ, tsupport u ⊆ s ∧ HasCompactSupport u ∧ ContDiff ℝ ∞ u ∧ range u ⊆ Icc 0 1 ∧ u x = 1$$$
Lean4
/-- 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`. -/
theorem exists_smooth_tsupport_subset {s : Set E} {x : E} (hs : s ∈ 𝓝 x) :
∃ f : E → ℝ, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1 :=
by
obtain ⟨d : ℝ, d_pos : 0 < d, hd : Euclidean.closedBall x d ⊆ s⟩ := Euclidean.nhds_basis_closedBall.mem_iff.1 hs
let c : ContDiffBump (toEuclidean x) :=
{ rIn := d / 2
rOut := d
rIn_pos := half_pos d_pos
rIn_lt_rOut := half_lt_self d_pos }
let f : E → ℝ := c ∘ toEuclidean
have f_supp : f.support ⊆ Euclidean.ball x d := by
intro y hy
have : toEuclidean y ∈ Function.support c := by simpa only [Function.mem_support, Function.comp_apply, Ne] using hy
rwa [c.support_eq] at this
have f_tsupp : tsupport f ⊆ Euclidean.closedBall x d :=
by
rw [tsupport, ← Euclidean.closure_ball _ d_pos.ne']
exact closure_mono f_supp
refine ⟨f, f_tsupp.trans hd, ?_, ?_, ?_, ?_⟩
· refine isCompact_of_isClosed_isBounded isClosed_closure ?_
have : IsBounded (Euclidean.closedBall x d) := Euclidean.isCompact_closedBall.isBounded
refine this.subset (Euclidean.isClosed_closedBall.closure_subset_iff.2 ?_)
exact f_supp.trans Euclidean.ball_subset_closedBall
· apply c.contDiff.comp
exact ContinuousLinearEquiv.contDiff _
· rintro t ⟨y, rfl⟩
exact ⟨c.nonneg, c.le_one⟩
· apply c.one_of_mem_closedBall
apply mem_closedBall_self
exact (half_pos d_pos).le
