measure_univ — Mathlib

English

For AddCircle T, the total measure of the whole space is ENNReal.ofReal T.

Русский

Для AddCircle T общая мера пространства равна ENNReal.ofReal T.

LaTeX

$$$\\displaystyle \\mathrm{volume}(\\mathrm{Set.univ}) = \\mathrm{ENNReal.ofReal}(T)$$$

Lean4

@[simp]
protected theorem measure_univ : volume (Set.univ : Set (AddCircle T)) = ENNReal.ofReal T :=
  by
  dsimp [volume]
  rw [← PositiveCompacts.coe_top]
  simp [addHaarMeasure_self (G := AddCircle T), -PositiveCompacts.coe_top]

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