Theorems · Theorem · measure theory

MeasureTheory.hausdorffMeasure_smul

∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {α : Type u_4}
  [inst_3 : SMul α X] [IsIsometricSMul α X] {d : ℝ} (c : α),
  (0 ≤ d ∨ Function.Surjective fun x => c • x) →
    ∀ (s : Set X), (MeasureTheory.Measure.hausdorffMeasure d) (c • s) = (MeasureTheory.Measure.hausdorffMeasure d) s

Defined in

Mathlib.MeasureTheory.Measure.Hausdorff

Cited by

0 results in Mathlib

Foundations

Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

EMetricSpaceMeasurableSpaceBorelSpaceSMulIsIsometricSMul