measure_map_restrict_apply — Mathlib

English

For s ⊆ α and a quotient map π: α → α/G, the pushforward of μ restricted to s by π satisfies (μ|s) map π (U) = μ((π^{-1}(U)) ∩ s) for measurable U.

Русский

Для подмножества s и отображения-проекции π: α → α/G, импликация мера по π от μ на s равна μ((π^{-1}(U)) ∩ s) для измеримой U.

LaTeX

$$\\bigl(\\mu \\restriction s\\bigr) \\mapsto π (U) = μ((π^{-1} U) \\cap s)$$

Lean4

@[to_additive addMeasure_map_restrict_apply]
theorem measure_map_restrict_apply (s : Set α) {U : Set (Quotient α_mod_G)} (meas_U : MeasurableSet U) :
    (μ.restrict s).map π U = μ ((π ⁻¹' U) ∩ s) := by
  rw [map_apply (f := π) (fun V hV ↦ measurableSet_quotient.mp hV) meas_U,
    Measure.restrict_apply (t := (Quotient.mk α_mod_G ⁻¹' U)) (measurableSet_quotient.mp meas_U)]

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