Compact neighborhoods in the positive phase

Every positive-phase point has a compact neighborhood of positive space-time measure contained in the positive-phase region.

theorem ESS.bu_short_positive_compact_neighborhood {scale : ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ buShortPositivePhaseRegion scale) : ∃ (S : Set CKN.Foundation.Parabolic.ParabolicPoint), IsCompact S ∧ z ∈ S ∧ S ⊆ buShortPositivePhaseRegion scale ∧ z ∈ interior S ∧ 0 < MeasureTheory.volume S

A positive-phase point lies in a compact positive-measure region contained entirely in the positive phase.