Theorems · Theorem · measure theory

Submodule.measurePreserving_measurableEquivProd

∀ {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] (s : Submodule ℝ V) (p : P),
  MeasureTheory.MeasurePreserving (⇑(s.measurableEquivProd p))
    (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V)) MeasureTheory.volume

Defined in

Mathlib.Geometry.Euclidean.Volume.Measure

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFiniteDimensionalMetricSpaceMeasurableSpaceBorelSpaceNormedAddTorsor