Theorems · Theorem · measure theory

BoundedContinuousFunction.toLp_denseRange

∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [inst_3 : BorelSpace α]
  (E : Type u_2) [inst_4 : NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal}
  [inst_5 : SecondCountableTopologyEither α E] [_i : Fact (1 ≤ p)] (𝕜 : Type u_3) [inst_6 : NormedRing 𝕜]
  [inst_7 : Module 𝕜 E] [inst_8 : IsBoundedSMul 𝕜 E] [NormedSpace ℝ E] [μ.WeaklyRegular]
  [inst_11 : MeasureTheory.IsFiniteMeasure μ], p ≠ ⊤ → DenseRange ⇑(BoundedContinuousFunction.toLp p μ 𝕜)

Defined in

Mathlib.MeasureTheory.Function.ContinuousMapDense

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormalSpaceMeasurableSpaceBorelSpaceNormedAddCommGroupSecondCountableTopologyEitherFactNormedRingModuleIsBoundedSMulNormedSpaceMeasureTheory.Measure.WeaklyRegularMeasureTheory.IsFiniteMeasure