English
The measure coming from the volume form associated to an orientation equals the standard volume measure.
Русский
Мера, порождённая формой объёма, сопряжённой к ориентации, совпадает со стандартной мерой объёма.
LaTeX
$$$o.volumeForm.measure = \\mathrm{volume}$.$$
Lean4
/-- In an oriented inner product space, the measure coming from the canonical volume form
associated to an orientation coincides with the volume. -/
theorem measure_eq_volume (o : Orientation ℝ F (Fin n)) : o.volumeForm.measure = volume :=
by
have A : o.volumeForm.measure (stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1 :=
Orientation.measure_orthonormalBasis o (stdOrthonormalBasis ℝ F)
rw [addHaarMeasure_unique o.volumeForm.measure (stdOrthonormalBasis ℝ F).toBasis.parallelepiped, A, one_smul]
simp only [volume, Basis.addHaar]
