∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [μ.OuterRegular],
  p ≠ ⊤ →
    ∀ {s u : Set α},
      IsClosed s →
        IsOpen u →
          s ⊆ u →
            μ s ≠ ⊤ →
              ∀ (c : E) {ε : ENNReal},
                ε ≠ 0 →
                  ∃ f,
                    Continuous f ∧
                      MeasureTheory.eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧
                        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MeasureTheory.MemLp f p μ