Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f g : α → E),
    Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ MemLp f p μ ∧ IsBounded (range f) →
      Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ IsBounded (range g) →
        Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f + g) ∧
          MemLp (f + g) p μ ∧ IsBounded (range (f + g))

pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f : α → E),
    Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ MemLp f p μ ∧ IsBounded (range f) →
      AEStronglyMeasurable f μ

pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      μ s < ∞ →
        ∀ {ε : ℝ≥0∞},
          ε ≠ 0 →
            ∃ g,
              eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧
                Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧
                  MemLp g p μ ∧ IsBounded (range g)

Tactic:
· rintro f g ⟨f_cont, f_mem, f_bd⟩ ⟨g_cont, g_mem, g_bd⟩
    refine ⟨f_cont.add g_cont, f_mem.add g_mem, ?_⟩
    let f' : α →ᵇ E := ⟨⟨f, f_cont⟩, Metric.isBounded_range_iff.1 f_bd⟩
    let g' : α →ᵇ E := ⟨⟨g, g_cont⟩, Metric.isBounded_range_iff.1 g_bd⟩
    exact (f' + g').isBounded_range

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f : α → E),
    Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ MemLp f p μ ∧ IsBounded (range f) →
      AEStronglyMeasurable f μ

α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      μ s < ∞ →
        ∀ {ε : ℝ≥0∞},
          ε ≠ 0 →
            ∃ g,
              eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧
                Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧
                  MemLp g p μ ∧ IsBounded (range g)