theorem TemperedDistribution.schwartz_partition_of_unity_vanishing {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℝ E] (u : TemperedDistribution E F) (h_local : ∀ (x : E), ∃ (s : Set E), Distribution.IsVanishingOn (⇑u) s ∧ IsOpen s ∧ x ∈ s) (ψ : SchwartzMap E ℂ) (hψ : HasCompactSupport ⇑ψ) : u ψ = 0

Schwartz partition-of-unity vanishing principle: a tempered distribution u annihilates any compactly supported Schwartz function ψ provided u vanishes locally everywhere, i.e. for every point x there is an open neighbourhood s ∋ x such that u is vanishing on s. The proof glues local vanishing via a smooth partition of unity subordinate to the cover.