undo typo

fpvandoorn · May 2, 2024 · a89997a · a89997a
1 parent 1e2429e
commit a89997a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Carleson/HomogeneousType.lean b/Carleson/HomogeneousType.lean
@@ -17,7 +17,7 @@ Should we assume `volume ≠ 0` / `IsOpenPosMeasure`? -/
 class IsSpaceOfHomogeneousType (X : Type*) (A : outParam ℝ) [PseudoMetricSpace X] extends
   MeasureSpace X, ProperSpace X, BorelSpace X,
   Regular (volume : Measure X), IsOpenPosMeasure (volume : Measure X) where
-    : ∀ (x : X) r, volume.real (ball x (2 * r)) ≤ A * volume.real (ball x r)
+  volume_ball_two_le_same : ∀ (x : X) r, volume.real (ball x (2 * r)) ≤ A * volume.real (ball x r)
 
 export IsSpaceOfHomogeneousType (volume_ball_two_le_same)