instIsAddHaarMeasureVolume — Mathlib

English

The standard volume on a finite-dimensional inner product space E is a left-invariant Haar measure.

Русский

Стандартный объём на конечномерном евклидовом пространстве является левой инвариантной мерой Хаара.

LaTeX

$$$IsAddHaarMeasure(volume)$$$

Lean4

instance [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] :
    IsAddHaarMeasure (volume : Measure E) :=
  isAddHaarMeasure_basis_addHaar
    _
      /- This instance should not be necessary, but Lean has difficulties to find it in product
      situations if we do not declare it explicitly. -/

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