∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d₁ d₂ : ℝ},
  d₁ ≤ d₂ → ∀ (s : Set X), (MeasureTheory.Measure.hausdorffMeasure d₂) s ≤ (MeasureTheory.Measure.hausdorffMeasure d₁) s