integrableOn_map_iff — Mathlib

English

For a measurable embedding e: α → β, integrability of f on s with respect to μ maps to integrability of f ∘ e on e^{-1}(s) with respect to μ.

Русский

Для допускаемого вложения e: α → β интегрируемость f на s по μ сопоставляется с интегрируемостью f ∘ e на e^{-1}(s) по μ.

LaTeX

$$IntegrableOn(f,s,μ.map e) ↔ IntegrableOn(f ∘ e, e^{-1}(s), μ)$$

Lean4

theorem _root_.MeasurableEmbedding.integrableOn_map_iff [MeasurableSpace β] {e : α → β} (he : MeasurableEmbedding e)
    {f : β → ε} {μ : Measure α} {s : Set β} : IntegrableOn f s (μ.map e) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ := by
  simp_rw [IntegrableOn, he.restrict_map, he.integrable_map_iff]

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