volume_eq_smul_haarAddCircle — Mathlib

English

The volume on AddCircle T equals the real number T times the Haar measure on AddCircle T, i.e., volume = (real T) • haarAddCircle.

Русский

Объём AddCircle T равен вещественному числу T, умноженному на меру Хаара: volume = Real(T) • haarAddCircle.

LaTeX

$$$$ \\text{volume} = \\operatorname{ofReal}(T) \\cdot \\text{haarAddCircle}. $$$$

Lean4

theorem volume_eq_smul_haarAddCircle : (volume : Measure (AddCircle T)) = ENNReal.ofReal T • (@haarAddCircle T _) :=
  rfl

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