Theorems · Theorem · measure theory

EuclideanGeometry.euclideanHausdorffMeasure_eq

∀ {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.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V) =
    MeasureTheory.Measure.map (⇑(IsometryEquiv.vaddConst p)) MeasureTheory.volume

We may want to endow an affine space with a MeasureSpace that transfers volume from its associated inner product space. If it is implemented, we can unify this lemma with the previous one.

Defined in

Mathlib.Geometry.Euclidean.Volume.Measure

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFiniteDimensionalMetricSpaceMeasurableSpaceBorelSpaceNormedAddTorsor