Tsupport Spatial Box

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.exists_spatial_box_of_tsupport_subset {Ω : Set Foundation.Parabolic.Vec3} {ψ : Foundation.Parabolic.Vec3 → ℝ} (hΩ : IsOpen Ω) (hψΩ : tsupport ψ ⊆ Ω) (hψc : HasCompactSupport ψ) : ∃ (Ω' : Set Foundation.Parabolic.Vec3), IsOpen Ω' ∧ tsupport ψ ⊆ Ω' ∧ IsCompact (closure Ω') ∧ closure Ω' ⊆ Ω

Given an open set Ω and a compactly supported function ψ whose topological support lies in Ω, there exists an open set Ω' containing tsupport ψ whose closure is compact and contained in Ω.