English
There exists a smooth function that is 0 near s and 1 near t in the neighborhood sense, with the range in [0,1].
Русский
Существет гладкая функция, которая обнуляется на окрестности s и достигает значения 1 на окрестности t, диапазон [0,1].
LaTeX
$$$\\exists f: C^\\infty(I,M; 𝓘(ℝ),ℝ), (f=0 \\,\\text{near} \\, s) ∧ (f=1 \\,\\text{near} \\, t) ∧ f(M) ⊆ [0,1]$$$
Lean4
/-- A `SmoothPartitionOfUnity` that consists of a single function, uniformly equal to one,
defined as an example for `Inhabited` instance. -/
def single (i : ι) (s : Set M) : SmoothPartitionOfUnity ι I M s :=
(BumpCovering.single i s).toSmoothPartitionOfUnity fun j => by
classical
rcases eq_or_ne j i with (rfl | h)
· simp only [contMDiff_one, ContinuousMap.coe_one, BumpCovering.coe_single, Pi.single_eq_same]
· simp only [contMDiff_zero, BumpCovering.coe_single, Pi.single_eq_of_ne h, ContinuousMap.coe_zero]
