Theorems · Theorem · measure theory

Orientation.measure_eq_volume

∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : MeasurableSpace F]
  [inst_3 : BorelSpace F] [inst_4 : FiniteDimensional ℝ F] {n : ℕ} [_i : Fact (Module.finrank ℝ F = n)]
  (o : Orientation ℝ F (Fin n)), o.volumeForm.measure = MeasureTheory.volume

In an oriented inner product space, the measure coming from the canonical volume form associated to an orientation coincides with the volume.

Defined in

Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFiniteDimensionalFact