Spatial restriction of a local product box

A support-containing box may be intersected with the open spatial region on which a pressure gradient is characterized, without changing its time interval or losing compact containment in the original domain.

theorem CKN.Core.Endgame.localBox_inter_spatial_open {Ω U V : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (hbox : localBox Ω I U J) (hV : IsOpen V) : localBox Ω I (U ∩ V) J

Intersecting the spatial factor with an open set preserves a local box.

theorem CKN.Core.Endgame.support_subset_inter_spatial_box {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {U V : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : tsupport φ ⊆ U ×ˢ J) (hspace : ∀ z ∈ tsupport φ, z.1 ∈ V) : tsupport φ ⊆ (U ∩ V) ×ˢ J

A spatial support bound is compatible with restriction of its local box.