instIsProbabilityMeasureUnitAddCircleVolume

English

The Haar measure on AddCircle is a probability measure; the total volume of AddCircle is 1.

Русский

Мера Хаара на AddCircle является вероятностной мерой; общая масса AddCircle равна 1.

LaTeX

$$$$ \\text{volume} \\; \\text{is a probability measure on AddCircle} $$$

Lean4

/-- The measure on `ℝ / ℤ` is a probability measure. -/
local instance : IsProbabilityMeasure (volume : Measure UnitAddCircle) :=
  inferInstanceAs (IsProbabilityMeasure AddCircle.haarAddCircle)

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