Theorems · Theorem · measure theory

Orientation.measure_orthonormalBasis

∀ {ι : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F]
  [inst_2 : MeasurableSpace F] [inst_3 : BorelSpace F] [inst_4 : Fintype ι] [inst_5 : FiniteDimensional ℝ F] {n : ℕ}
  [_i : Fact (Module.finrank ℝ F = n)] (o : Orientation ℝ F (Fin n)) (b : OrthonormalBasis ι ℝ F),
  o.volumeForm.measure (parallelepiped ⇑b) = 1

The volume form coming from an orientation in an inner product space gives measure 1 to the parallelepiped associated to any orthonormal basis. This is a rephrasing of abs_volumeForm_apply_of_orthonormal in terms of measures.

Defined in

Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFintypeFiniteDimensionalFact