aestronglyMeasurable_comp_iff — Mathlib

English

For measure-preserving f with measurable embedding, AEStronglyMeasurable(g ∘ f) iff AEStronglyMeasurable(g).

Русский

Для меросохраняющего f и измеримого вложения, AEStronglyMeasurable(g ∘ f) ⇔ AEStronglyMeasurable(g).

LaTeX

$$$$\\text{AEStronglyMeasurable}(g \\circ f) \\iff \\text{AEStronglyMeasurable}(g).$$$$

Lean4

theorem aestronglyMeasurable_comp_iff {β : Type*} {f : α → β} {mα : MeasurableSpace α} {μa : Measure α}
    {mβ : MeasurableSpace β} {μb : Measure β} (hf : MeasurePreserving f μa μb) (h₂ : MeasurableEmbedding f)
    {g : β → γ} : AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable g μb := by
  rw [← hf.map_eq, h₂.aestronglyMeasurable_map_iff]

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