Singleton Null

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

theorem CKN.Foundation.Parabolic.Integration.volume_singleton_parabolicPoint (z : ParabolicPoint) : MeasureTheory.volume {z} = 0

A single parabolic point has zero Lebesgue volume.