aemeasurable_map_equiv_iff — Mathlib

English

Let e be a measurable equivalence between α and β. For any function f: β → γ, f is almost everywhere measurable with respect to μ.map e if and only if f ∘ e is almost everywhere μ-measurable.

Русский

Пусть e — измеримое эквивалентное отображение между пространствами α и β. Для любой функции f: β → γ а.е.-измеримость f относительно μ.map e эквивалентна а.е.-измеримости f ∘ e относительно μ.

LaTeX

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

Lean4

theorem aemeasurable_map_equiv_iff (e : α ≃ᵐ β) {f : β → γ} : AEMeasurable f (μ.map e) ↔ AEMeasurable (f ∘ e) μ :=
  e.measurableEmbedding.aemeasurable_map_iff

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