Theorems · Theorem · measure theory

IsometryEquiv.measurePreserving_euclideanHausdorffMeasure

∀ {X : Type u_1} {Y : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
  [inst_3 : EMetricSpace Y] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] (e : X ≃ᵢ Y) (d : ℕ),
  MeasureTheory.MeasurePreserving (⇑e) (MeasureTheory.Measure.euclideanHausdorffMeasure d)
    (MeasureTheory.Measure.euclideanHausdorffMeasure d)

Defined in

Mathlib.Geometry.Euclidean.Volume.Measure

Cited by

2 results in Mathlib

Foundations

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

Assumes

EMetricSpaceMeasurableSpaceBorelSpaceEMetricSpaceMeasurableSpaceBorelSpace