theorem SmoothPartitionOfUnity.exists_smooth_finitePartition_of_isCompact {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {A : Type u_2} {U : A → Set E} {K : Set E} (hU : ∀ (a : A), IsOpen (U a)) (hK : IsCompact K) (hKU : K ⊆ ⋃ (a : A), U a) : ∃ (N : ℕ) (φ : Fin N → E → ℝ) (a : Fin N → A), (∀ (i : Fin N), ContDiff ℝ (↑⊤) (φ i)) ∧ (∀ (i : Fin N) (x : E), 0 ≤ φ i x) ∧ (∀ (i : Fin N) (x : E), φ i x ≤ 1) ∧ (∀ (i : Fin N), tsupport (φ i) ⊆ U (a i)) ∧ ∃ (V : Set E), IsOpen V ∧ K ⊆ V ∧ ∀ x ∈ V, ∑ i : Fin N, φ i x = 1

Proposition 8.7 of Melrose: existence of a finite smooth partition of unity on a compact set K in a finite-dimensional Euclidean space, subordinate to a given open cover {U a}. The output gives finitely many C^∞ cutoffs φ_i valued in [0,1] with tsupport (φ i) contained in some U (a i), summing to 1 on an open neighbourhood of K.

theorem exists_continuous_partition_of_isCompact {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [T2Space X] {ι : Type u_2} [Fintype ι] {U : ι → Set X} (hU : ∀ (i : ι), IsOpen (U i)) {K : Set X} (hK : IsCompact K) (hKU : K ⊆ ⋃ (i : ι), U i) : ∃ (f : ι → C(X, ℝ)), (∀ (i : ι) (x : X), 0 ≤ (f i) x) ∧ (∀ (i : ι) (x : X), (f i) x ≤ 1) ∧ (∀ (i : ι), HasCompactSupport ⇑(f i)) ∧ (∀ (i : ι), tsupport ⇑(f i) ⊆ U i) ∧ ∃ (V : Set X), IsOpen V ∧ K ⊆ V ∧ ∀ x ∈ V, ∑ i : ι, (f i) x = 1

Continuous partition of unity variant of Proposition 8.7: on a locally compact Hausdorff space X, any compact K covered by finitely many open sets U i admits a continuous partition of unity subordinate to the cover, with each f i having compact support.