measure_preimage — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem measure_preimage {f : α → β} (hf : MeasurePreserving f μa μb) {s : Set β} (hs : NullMeasurableSet s μb) :
    μa (f ⁻¹' s) = μb s := by
  rw [← hf.map_eq] at hs ⊢
  rw [map_apply₀ hf.1.aemeasurable hs]

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