projection_respects_measure_apply

English

For any measurable set U of the quotient space, μ(U) equals ν(π^{-1}(U) ∩ t).

Русский

Для любого измеримого множества U в пространстве-квазиобразе, μ(U) равно ν(π^{-1}(U) ∩ t).

LaTeX

$$μ U = ν (π^{-1} U ∩ t)$$

Lean4

@[to_additive addProjection_respects_measure_apply]
theorem projection_respects_measure_apply {ν : Measure α} (μ : Measure (Quotient α_mod_G))
    [i : QuotientMeasureEqMeasurePreimage ν μ] {t : Set α} (fund_dom_t : IsFundamentalDomain G t ν)
    {U : Set (Quotient α_mod_G)} (meas_U : MeasurableSet U) : μ U = ν (π ⁻¹' U ∩ t) := by
  rw [fund_dom_t.projection_respects_measure (μ := μ), measure_map_restrict_apply ν t meas_U]

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