Relative closedness of the singular set

Paper label lem:S-closed: for a suitable weak solution on the space-time carrier 𝒪 = Ω × I, the singular set is relatively closed in 𝒪. The proof is the paper's: the regular points form an open set, because the open neighbourhood that witnesses regularity at one point witnesses it at every point of that same neighbourhood; the singular set is then the trace on 𝒪 of the complement, a closed set.

theorem CKN.isOpen_regularSet (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : IsOpen {z : Foundation.Parabolic.ParabolicPoint | IsRegularPoint Ω I u z}

Paper label lem:S-closed: the set of regular points is open. If z₀ is regular, the open set N supplied by def:regular consists of regular points, because it is contained in spaceTimeSet Ω I and its witness w and exponent γ serve every point of N equally.

theorem CKN.singularSet_eq_diff (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : SingularSet Ω I u = spaceTimeSet Ω I \ {z : Foundation.Parabolic.ParabolicPoint | IsRegularPoint Ω I u z}

Paper label def:regular: the singular set is the complement of the regular set inside the space-time carrier spaceTimeSet Ω I.

theorem CKN.isClosed_singularSet_within (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : ∃ (C : Set Foundation.Parabolic.ParabolicPoint), IsClosed C ∧ SingularSet Ω I u = C ∩ spaceTimeSet Ω I

Paper label lem:S-closed: the singular set is relatively closed in the space-time carrier spaceTimeSet Ω I, that is, it is the trace on the carrier of a closed set. The closed set is the complement of the regular set.