measureReal_preimage — Mathlib

English

If f preserves μa to μb and s is μb-null-measurable, then μa.real(f^{-1}(s)) = μb.real(s).

Русский

Если f сохраняет μа→μb и s μb-нулеизмеримо, то μa.real(f^{-1}(s)) = μb.real(s).

LaTeX

$$$\text{MeasurePreserving } f\, μ_a\, μ_b \rightarrow \forall s,\; NullMeasurableSet(s, μ_b) \rightarrow μ_a.real(f^{-1}(s)) = μ_b.real(s)$$$

Lean4

theorem measureReal_preimage {f : α → β} (hf : MeasurePreserving f μa μb) {s : Set β} (hs : NullMeasurableSet s μb) :
    μa.real (f ⁻¹' s) = μb.real s := by simp [measureReal_def, measure_preimage hf hs]

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