Passing from closed to strict halfspaces

theorem Grunbaum.volume_inter_le_eq_volume_inter_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [MeasureTheory.volume.IsAddHaarMeasure] (K : Set E) (hK : MeasurableSet K) (L : E →L[ℝ] ℝ) (hL : L ≠ 0) (t : ℝ) : MeasureTheory.volume (K ∩ {x : E | t ≤ L x}) = MeasureTheory.volume (K ∩ {x : E | t < L x})

A nonzero linear functional has no boundary mass, so closed and strict halfspaces cut the same volume from every measurable set.