volume_parallelepiped — Mathlib

English

An orthonormal basis defines a Haar measure; the associated addHaar equals the volume.

Русский

Ортонормированный базис задаёт меру Хаара; связанная мера addHaar совпадает с объёмом.

LaTeX

$$$\\text{basis} \\toAddHaar = \\text{volume}$.$$

Lean4

/-- The volume measure in a finite-dimensional inner product space gives measure `1` to the
parallelepiped spanned by any orthonormal basis. -/
theorem volume_parallelepiped (b : OrthonormalBasis ι ℝ F) : volume (parallelepiped b) = 1 :=
  by
  haveI : Fact (finrank ℝ F = finrank ℝ F) := ⟨rfl⟩
  let o := (stdOrthonormalBasis ℝ F).toBasis.orientation
  rw [← o.measure_eq_volume]
  exact o.measure_orthonormalBasis b

Похожие утверждения