Local Box #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.caccioppoli_localBox_of_compact_subset
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{K : Set Foundation.Parabolic.ParabolicPoint}
(hΩ : IsOpen Ω)
(hI : IsOpen I)
(hIord : I.OrdConnected)
(hK : IsCompact K)
(hKsub : K ⊆ spaceTimeSet Ω I)
:
∃ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I Ω' J ∧ K ⊆ spaceTimeSet Ω' J
A compact subset of an open space-time carrier is contained in a compact local box.