Theorems · Theorem · measure theory

MeasureTheory.integral_indicatorConstLp

∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {t : Set X} {μ : MeasureTheory.Measure X} [CompleteSpace E] {p : ENNReal} (ht : MeasurableSet t) (hμt : μ t ≠ ⊤)
  (e : E), ∫ (x : X), ↑↑(MeasureTheory.indicatorConstLp p ht hμt e) x ∂μ = μ.real t • e

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace