quotientMeasureEqMeasurePreimage — Mathlib

English

If a fundamental domain s exists for G acting on α, then any μ with μ = (ν|s).map π satisfies QuotientMeasureEqMeasurePreimage with ν.

Русский

Если существует фундаментальная область s для действия G на α, то любая мера μ = (ν|s).map π удовлетворяет QuotientMeasureEqMeasurePreimage по ν.

LaTeX

$$$IsFundamentalDomain(G,s,ν) \\Rightarrow (μ = (ν|_{s}).map π) \\Rightarrow QuotientMeasureEqMeasurePreimage\\nu\\mu.$$$

Lean4

/-- One can prove `QuotientMeasureEqMeasurePreimage` by checking behavior with respect to a single
fundamental domain. -/
@[to_additive]
theorem quotientMeasureEqMeasurePreimage {μ : Measure (Quotient α_mod_G)} {s : Set α}
    (fund_dom_s : IsFundamentalDomain G s ν) (h : μ = (ν.restrict s).map π) : QuotientMeasureEqMeasurePreimage ν μ := by
  simpa [h] using fund_dom_s.quotientMeasureEqMeasurePreimage_quotientMeasure

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