Revert whitespace

eric-wieser · web-flow · commit f4c32e026927 · 2024-02-25T23:07:02.000Z
diff --git a/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean b/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
@@ -133,6 +133,7 @@ def multiplicity (E : Type*) [NormedAddCommGroup E] :=
 section
 
 variable [NormedSpace ℝ E] [FiniteDimensional ℝ E]
+
 /-- Any `1`-separated set in the ball of radius `2` has cardinality at most `5 ^ dim`. This is
 useful to show that the supremum in the definition of `Besicovitch.multiplicity E` is
 well behaved. -/
