English
If two measures on the quotient space α mod G both satisfy the quotient-measure-preimage relation with a fixed upstairs measure ν, then those two measures are equal.
Русский
Если две меры на фактор-пространстве α/G удовлетворяют отношению QuotientMeasureEqMeasurePreimage с заданной верхней мерой ν, то эти две меры равны.
LaTeX
$$$\\forall \\mu,\\mu' : \\operatorname{Measure}(\\Quotient(\\MulAction.orbitRel G α))\\\\, [\\\\QuotientMeasureEqMeasurePreimage \\nu \\mu] \\\\ [\\\\QuotientMeasureEqMeasurePreimage \\nu \\mu'] \\Rightarrow \\mu = \\mu'.,$$
Lean4
/-- Any two measures satisfying `QuotientMeasureEqMeasurePreimage` are equal. -/
@[to_additive]
theorem unique [hasFun : HasFundamentalDomain G α ν] (μ μ' : Measure (Quotient α_mod_G))
[QuotientMeasureEqMeasurePreimage ν μ] [QuotientMeasureEqMeasurePreimage ν μ'] : μ = μ' :=
by
obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain
rw [h𝓕.projection_respects_measure (μ := μ), h𝓕.projection_respects_measure (μ := μ')]
