Theorems · Theorem · measure theory

MeasureTheory.euclideanHausdorffMeasure_homothety_preimage

∀ {𝕜 : Type u_3} {V : Type u_4} {P : Type u_5} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : MeasurableSpace P] [inst_4 : MetricSpace P] [inst_5 : NormedAddTorsor V P]
  [inst_6 : BorelSpace P] (d : ℕ) (x : P) {c : 𝕜},
  c ≠ 0 →
    ∀ (s : Set P),
      (MeasureTheory.Measure.euclideanHausdorffMeasure d) (⇑(AffineMap.homothety x c) ⁻¹' s) =
        ‖c‖₊⁻¹ ^ d • (MeasureTheory.Measure.euclideanHausdorffMeasure d) s

Defined in

Mathlib.Geometry.Euclidean.Volume.Measure

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedAddCommGroupNormedSpaceMeasurableSpaceMetricSpaceNormedAddTorsorBorelSpace