Theorems · Theorem · measure theory

MeasurableEmbedding.integrable_map_iff

∀ {α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : MeasurableSpace δ] [inst_1 : TopologicalSpace ε] [inst_2 : ContinuousENorm ε] {f : α → δ},
  MeasurableEmbedding f →
    ∀ {g : δ → ε}, MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Integrable (g ∘ f) μ

Defined in

Mathlib.MeasureTheory.Function.L1Space.Integrable

Cited by

6 results in Mathlib

Foundations

Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceContinuousENorm