Theorems · Definition · measure theory

MeasureTheory.Lp.simpleFunc.indicatorConst

{α : Type u_1} →
  {E : Type u_4} →
    [inst : MeasurableSpace α] →
      [inst_1 : NormedAddCommGroup E] →
        (p : ENNReal) →
          {μ : MeasureTheory.Measure α} →
            {s : Set α} → MeasurableSet s → μ s ≠ ⊤ → E → ↥(MeasureTheory.Lp.simpleFunc E p μ)

The characteristic function of a finite-measure measurable set s, as an Lp simple function.

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

14 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroup