English
If the covolume is finite, then the quotient measure μ is finite.
Русский
Если ковольюм конечен, то мера на факторпространстве μ конечна.
LaTeX
$$$covolume(G,\\alpha,\\nu) \\neq \\infty \\Rightarrow IsFiniteMeasure(μ).$$$
Lean4
/-- If a measure `μ` on a quotient satisfies `QuotientVolumeEqVolumePreimage` with respect to a
sigma-finite measure, then it is itself `SigmaFinite`. -/
@[to_additive MeasureTheory.instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace]
instance [SigmaFinite (volume : Measure α)] [HasFundamentalDomain G α] (μ : Measure (Quotient α_mod_G))
[QuotientMeasureEqMeasurePreimage volume μ] : SigmaFinite μ :=
QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient (ν := (volume : Measure α)) (μ := μ)
