Theorems · Definition · measure theory

MeasureTheory.Lp.simpleFunc

{α : Type u_1} →
  (E : Type u_4) →
    [inst : MeasurableSpace α] →
      [inst_1 : NormedAddCommGroup E] →
        (p : ENNReal) → (μ : MeasureTheory.Measure α) → AddSubgroup ↥(MeasureTheory.Lp E p μ)

Lp.simpleFunc is a subspace of Lp consisting of equivalence classes of an integrable simple function.

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

122 results in Mathlib

Foundations

Depth 222 from the axioms, rests on 6,104 definitions · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceNormedAddCommGroup