Theorems · Theorem · measure theory

MeasureTheory.Lp.simpleFunc.denseRange_coeSimpleFuncNonnegToLpNonneg

∀ {α : Type u_1} [inst : MeasurableSpace α] (p : ENNReal) (μ : MeasureTheory.Measure α) (G : Type u_7)
  [inst_1 : NormedAddCommGroup G] [inst_2 : PartialOrder G] [hp : Fact (1 ≤ p)],
  p ≠ ⊤ → DenseRange (MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg p μ G)

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupPartialOrderFact