aemeasurable_iff_measurable — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem aemeasurable_iff_measurable [μ.IsComplete] : AEMeasurable f μ ↔ Measurable f :=
  ⟨fun h => h.nullMeasurable.measurable_of_complete, fun h => h.aemeasurable⟩

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