Local Box

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

def CKN.localBox (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ) : Prop

Compactly interior spatial and time subdomains used by paper label def:sws.

Equations

• CKN.localBox Ω I Ω' J = (IsOpen Ω' ∧ IsCompact (closure Ω') ∧ closure Ω' ⊆ Ω ∧ J.OrdConnected ∧ IsCompact (closure J) ∧ closure J ⊆ I)