integrableOn_comp_preimage — Mathlib

English

For a measurable embedding e, IntegrableOn f s μ is equivalent to IntegrableOn (f ∘ e) (preimage e s) (μ.comap e).

Русский

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

LaTeX

$$IntegrableOn f s μ ↔ IntegrableOn (f ∘ e) (preimage e s) (μ.comap e)$$

Lean4

theorem integrableOn_comp_preimage [MeasurableSpace β] {e : α → β} {ν} (h₁ : MeasurePreserving e μ ν)
    (h₂ : MeasurableEmbedding e) {f : β → ε} {s : Set β} : IntegrableOn (f ∘ e) (e ⁻¹' s) μ ↔ IntegrableOn f s ν :=
  (h₁.restrict_preimage_emb h₂ s).integrable_comp_emb h₂

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