aemeasurable_restrict_iff_comap_subtype

English

For a measurable s, AEMeasurable f on μ.restrict s is equivalent to AEMeasurable (f ∘ ↑) on comap ↑ μ.

Русский

Для измеримого s AЕ-измеримость f на μ|_s эквивалентна AЕ-измеримости f∘(↑) на comap ↑ μ.

LaTeX

$$$\mathrm{AEMeasurable}(f, \mu\restriction s) \iff \mathrm{AEMeasurable}(f \circ (\uparrow) : s \to \beta, \mathrm{comap}(\uparrow, \mu))$$$

Lean4

theorem aemeasurable_restrict_iff_comap_subtype {s : Set α} (hs : MeasurableSet s) {μ : Measure α} {f : α → β} :
    AEMeasurable f (μ.restrict s) ↔ AEMeasurable (f ∘ (↑) : s → β) (comap (↑) μ) := by
  rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).aemeasurable_map_iff]

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