English
There exists a smooth function with support equal to s, range in [0,1], equal to 1 on t, etc.
Русский
Существует гладкая функция с опорой s и диапазоном [0,1], равная 1 на t.
LaTeX
$$$\\exists f: M→ℝ, ContMDiff I 𝓘(ℝ) ∞ f ∧ supp f = s ∧ range f ⊆ [0,1] ∧ (∀ x∈t, f x = 1)$$$
Lean4
/-- Given an open set `s` containing a closed set `t` in a finite-dimensional real manifold, there
exists a smooth function with support equal to `s`, taking values in `[0,1]`, and equal to `1`
exactly on `t`. -/
theorem exists_msmooth_support_eq_eq_one_iff {s t : Set M} (hs : IsOpen s) (ht : IsClosed t) (h : t ⊆ s) :
∃ f : M → ℝ, ContMDiff I 𝓘(ℝ) ∞ f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ (∀ x, x ∈ t ↔ f x = 1) := by
/- Take `f` with support equal to `s`, and `g` with support equal to `tᶜ`. Then `f / (f + g)`
satisfies the conclusion of the theorem. -/
rcases hs.exists_msmooth_support_eq I with ⟨f, f_supp, f_diff, f_pos⟩
rcases ht.isOpen_compl.exists_msmooth_support_eq I with ⟨g, g_supp, g_diff, g_pos⟩
have A : ∀ x, 0 < f x + g x := by
intro x
by_cases xs : x ∈ support f
· have : 0 < f x := lt_of_le_of_ne (f_pos x) (Ne.symm xs)
linarith [g_pos x]
· have : 0 < g x := by
classical
apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
rw [← mem_support, g_supp]
contrapose! xs
exact h.trans f_supp.symm.subset (by simpa using xs)
linarith [f_pos x]
refine
⟨fun x ↦ f x / (f x + g x), ?_, ?_, ?_, ?_⟩
-- show that `f / (f + g)` is smooth
·
exact
f_diff.div₀ (f_diff.add g_diff)
(fun x ↦ ne_of_gt (A x))
-- show that the range is included in `[0, 1]`
· refine range_subset_iff.2 (fun x ↦ ⟨div_nonneg (f_pos x) (A x).le, ?_⟩)
apply div_le_one_of_le₀ _ (A x).le
simpa only [le_add_iff_nonneg_right] using g_pos x
· have B : support (fun x ↦ f x + g x) = univ := eq_univ_of_forall (fun x ↦ (A x).ne')
simp only [support_div, f_supp, B, inter_univ]
-- show that the function equals one exactly on `t`
· intro x
simp [div_eq_one_iff_eq (A x).ne', left_eq_add, ← notMem_support, g_supp]
