Theorems · Theorem · measure theory

MeasureTheory.fst_integral_withLp

∀ {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)} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [CompleteSpace F],
  MeasureTheory.Integrable f μ → (∫ (x : X), f x ∂μ).fst = ∫ (x : X), (f x).fst ∂μ

Defined in

Mathlib.MeasureTheory.SpecificCodomains.WithLp

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactNormedAddCommGroupNormedAddCommGroupNormedSpaceNormedSpaceCompleteSpace