integrableOn_map_equiv — Mathlib

English

If e is a measurable equivalence, then integrability of f on s w.r.t. μ maps to integrability of f ∘ e on e^{-1}(s) w.r.t. μ.

Русский

Если e — измеримое эквив, то интегрируемость f на s по μ соответствует интегрируемости f ∘ e на e^{-1}(s) по μ.

LaTeX

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

Lean4

theorem integrableOn_map_equiv [MeasurableSpace β] (e : α ≃ᵐ β) {f : β → ε} {μ : Measure α} {s : Set β} :
    IntegrableOn f s (μ.map e) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ := by
  simp only [IntegrableOn, e.restrict_map, integrable_map_equiv e]

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