integrableOn_iff_comap_subtypeVal

English

For a measurable set s, IntegrableOn f s μ is equivalent to Integrable (f ∘ Subtype.val) (Measure.comap Subtype.val μ) on the subtype s.

Русский

Для измеримого множества s Интегрируемость f на s по μ эквивалентна интегрируемости f ∘ Subtype.val на подтипе s по μ comap Subtype.val.

LaTeX

$$IntegrableOn f s μ ↔ Integrable (f ∘ Subtype.val) (Subtype.val) (μ.comap Subtype.val)$$

Lean4

theorem integrableOn_iff_comap_subtypeVal (hs : MeasurableSet s) :
    IntegrableOn f s μ ↔ Integrable (f ∘ (↑) : s → ε) (μ.comap (↑)) := by
  rw [← (MeasurableEmbedding.subtype_coe hs).integrableOn_range_iff_comap, Subtype.range_val]

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