aemeasurable_comp_iff — Mathlib

English

Let f be measure-preserving with a MeasurableEmbedding; for any s, restricting to f^{-1}(s) and s preserves measure.

Русский

Пусть f сохраняет меру и имеет измеримое вложение; для любого s сохранение меры на предобразе сохраняется.

LaTeX

$$$hf: MeasurePreserving f μa μb \\wedge h₂: MeasurableEmbedding f \\Rightarrow \\forall s, MeasurePreserving f (μa.restrict (f^{-1} s)) (μb.restrict s)$$$

Lean4

theorem aemeasurable_comp_iff {f : α → β} (hf : MeasurePreserving f μa μb) (h₂ : MeasurableEmbedding f) {g : β → γ} :
    AEMeasurable (g ∘ f) μa ↔ AEMeasurable g μb := by rw [← hf.map_eq, h₂.aemeasurable_map_iff]

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