aemeasurable_map_iff — Mathlib

English

If g is a MeasurableEmbedding, AEMeasurable g (μ.map f) is equivalent to AEMeasurable (g ∘ f) μ.

Русский

Если g — измеримое вложение, AЕ-измеримость g относительно μ.map f эквивалентна AЕ-измеримости g∘f относительно μ.

LaTeX

$$$\mathrm{MeasurableEmbedding}(g) \rightarrow (\mathrm{AEMeasurable}(g, \mu\map f) \iff \mathrm{AEMeasurable}(g \circ f, \mu))$$$

Lean4

theorem aemeasurable_map_iff {g : β → γ} (hf : MeasurableEmbedding f) :
    AEMeasurable g (μ.map f) ↔ AEMeasurable (g ∘ f) μ :=
  by
  refine ⟨fun H => H.comp_measurable hf.measurable, ?_⟩
  rintro ⟨g₁, hgm₁, heq⟩
  rcases hf.exists_measurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩
  exact ⟨g₂, hgm₂, hf.ae_map_iff.2 heq⟩

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