Theorems · Theorem · measure theory

MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume

∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  (ν : MeasureTheory.Measure α) [Countable G] [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α ν]
  {s : Set α}, MeasureTheory.IsAddFundamentalDomain G s ν → MeasureTheory.addCovolume G α ν = ν s

The addCovolume can be computed by taking the volume of any given additive fundamental domain s.

Defined in

Mathlib.MeasureTheory.Group.FundamentalDomain

Cited by

5 results in Mathlib

Foundations

Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddActionMeasurableSpaceCountableMeasurableConstVAddMeasureTheory.VAddInvariantMeasure