Theorems · Theorem · measure theory

MeasureTheory.integrable_prodLp_iff

∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  {f : X → WithLp q (E × F)},
  MeasureTheory.Integrable f μ ↔
    MeasureTheory.Integrable (fun x => (f x).fst) μ ∧ MeasureTheory.Integrable (fun x => (f x).snd) μ

Defined in

Mathlib.MeasureTheory.SpecificCodomains.WithLp

Cited by

3 results in Mathlib

Foundations

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

Assumes

FactNormedAddCommGroupNormedAddCommGroup