Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.integrable_vectorMeasure_prodMk_left

∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.VectorMeasure X E}
  {ν : MeasureTheory.VectorMeasure Y F} [MeasureTheory.IsFiniteMeasure μ.variation] {s : Set (X × Y)},
  MeasurableSet s → μ.Integrable fun x => ν (Prod.mk x ⁻¹' s)

Defined in

Mathlib.MeasureTheory.VectorMeasure.Prod

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupNormedSpaceMeasureTheory.IsFiniteMeasure