projection_respects_measure — Mathlib

English

If t is a fundamental domain for ν, then the quotient projection π respects measure in the sense that μ = (ν|_t).map π.

Русский

Если t — фундаментальная область для ν, то проекция квартивации π сохраняет меру: μ = (ν|_t).map π.

LaTeX

$$μ = (ν.restrict t).map π$$

Lean4

@[to_additive addProjection_respects_measure]
theorem projection_respects_measure {ν : Measure α} (μ : Measure (Quotient α_mod_G))
    [i : QuotientMeasureEqMeasurePreimage ν μ] {t : Set α} (fund_dom_t : IsFundamentalDomain G t ν) :
    μ = (ν.restrict t).map π :=
  i.projection_respects_measure' t fund_dom_t

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