A finite smooth partition of unity on a compact set

Elementary construction of finitely many smooth compactly supported functions, each supported inside one member of a given open cover of a compact set, whose sum equals 1 on that compact set. The construction multiplies bump functions telescopically, so no manifold partition-of-unity machinery is needed.

theorem CKN.exists_smooth_partition_of_unity_of_isCompact {d : ℕ} {ι : Type u_1} {K : Set (Vec d)} (hK : IsCompact K) (V : ι → Set (Vec d)) (hV : ∀ (b : ι), IsOpen (V b)) (hcover : K ⊆ ⋃ (b : ι), V b) : ∃ (N : ℕ) (χ : ℕ → Vec d → ℝ), (∀ (k : ℕ), ContDiff ℝ (↑⊤) (χ k)) ∧ (∀ (k : ℕ), HasCompactSupport (χ k)) ∧ (∀ k ∈ Finset.range N, ∃ (b : ι), tsupport (χ k) ⊆ V b) ∧ ∀ x ∈ K, ∑ k ∈ Finset.range N, χ k x = 1

On a compact set covered by open sets there are finitely many smooth compactly supported functions, each supported inside one member of the cover, whose sum is identically one on the compact set.