English
If the i-th bump is zero at x, then the i-th partition function is zero at x.
Русский
Если i-я шип-функция равна нулю в точке x, то φ_i(x)=0.
LaTeX
$$$fs(i,x)=0 \\Rightarrow fs.toSmoothPartitionOfUnity(i,x)=0$$$
Lean4
/-- Given two disjoint closed sets `s, t` in a Hausdorff normal σ-compact finite-dimensional
manifold `M`, there exists a smooth function `f : M → [0,1]` that vanishes in a neighbourhood of `s`
and is equal to `1` in a neighbourhood of `t`. -/
theorem exists_smooth_zero_one_nhds_of_isClosed [T2Space M] [NormalSpace M] [SigmaCompactSpace M] {s t : Set M}
(hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
∃ f : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, (∀ᶠ x in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ x in 𝓝ˢ t, f x = 1) ∧ ∀ x, f x ∈ Icc 0 1 :=
by
obtain ⟨u, u_op, hsu, hut⟩ :=
normal_exists_closure_subset hs ht.isOpen_compl (subset_compl_iff_disjoint_left.mpr hd.symm)
obtain ⟨v, v_op, htv, hvu⟩ := normal_exists_closure_subset ht isClosed_closure.isOpen_compl (subset_compl_comm.mp hut)
obtain ⟨f, hfu, hfv, hf⟩ :=
exists_smooth_zero_one_of_isClosed I isClosed_closure isClosed_closure (subset_compl_iff_disjoint_left.mp hvu)
refine ⟨f, ?_, ?_, hf⟩
· exact eventually_of_mem (mem_of_superset (u_op.mem_nhdsSet.mpr hsu) subset_closure) hfu
· exact eventually_of_mem (mem_of_superset (v_op.mem_nhdsSet.mpr htv) subset_closure) hfv
