∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [μ.WeaklyRegular],
  p ≠ ⊤ →
    ∀ {f : α → E},
      MeasureTheory.MemLp f p μ →
        ∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, MeasureTheory.eLpNorm (f - ⇑g) p μ ≤ ε ∧ MeasureTheory.MemLp (⇑g) p μ