Stability Local Box Enclosure

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_localBox_compact_enclosure {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (hbox : localBox Ω I Ω' J) : ∃ (K : Set Foundation.Parabolic.ParabolicPoint), IsCompact K ∧ spaceTimeSet Ω' J ⊆ K ∧ K ⊆ spaceTimeSet Ω I

Every local box lies in a compact product set still contained in the space-time carrier.