Theorems · Theorem · measure theory

MeasureTheory.setIntegral_indicatorConstLp

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

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace