Space Time Set

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

def CKN.spaceTimeSet (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) : Set Foundation.Parabolic.ParabolicPoint

The open space-time carrier Ω × I from paper label def:sws.

Equations

• CKN.spaceTimeSet Ω I = Ω ×ˢ I