Theorems · Theorem · measure theory

EuclideanGeometry.measurePreserving_vaddConst

∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MetricSpace P]
  [inst_6 : MeasurableSpace P] [inst_7 : BorelSpace P] [inst_8 : NormedAddTorsor V P] (p : P),
  MeasureTheory.MeasurePreserving (⇑(IsometryEquiv.vaddConst p)) MeasureTheory.volume
    (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V))

Defined in

Mathlib.Geometry.Euclidean.Volume.Measure

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFiniteDimensionalMetricSpaceMeasurableSpaceBorelSpaceNormedAddTorsor