English
For an open set s in a finite-dimensional manifold, there exists a nonnegative smooth function with support exactly s.
Русский
Для открытого множества s на конечном размерном многообразии существует неотрицательная гладкая функция с опорой ровно в s.
LaTeX
$$$\\exists f: M→ℝ, f^{(∞)} ≥ 0, \\operatorname{supp} f = s$$$
Lean4
theorem exists_msmooth_support_eq_aux {s : Set H} (hs : IsOpen s) :
∃ f : H → ℝ, f.support = s ∧ ContMDiff I 𝓘(ℝ) ∞ f ∧ Set.range f ⊆ Set.Icc 0 1 :=
by
have h's : IsOpen (I.symm ⁻¹' s) := I.continuous_symm.isOpen_preimage _ hs
rcases h's.exists_smooth_support_eq with ⟨f, f_supp, f_diff, f_range⟩
refine ⟨f ∘ I, ?_, ?_, ?_⟩
· rw [support_comp_eq_preimage, f_supp, ← preimage_comp]
simp only [ModelWithCorners.symm_comp_self, preimage_id_eq, id_eq]
· exact f_diff.comp_contMDiff contMDiff_model
· exact Subset.trans (range_comp_subset_range _ _) f_range
