case h_bound
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
⊢ ∀ (n : ι),
    ∀ᵐ (t : ℝ),
      t ∈ Ι a b →
        ‖↑(f n) t‖ ≤ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f n)‖

case bound_summable
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι a b →
      Summable fun n =>
        ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f n)‖

case bound_integrable
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
⊢ IntervalIntegrable
    (fun t =>
      ∑' (n : ι), ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f n)‖)
    volume a b

case h_lim
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
⊢ ∀ᵐ (t : ℝ), t ∈ Ι a b → HasSum (fun n => ↑(f n) t) (∑' (i : ι), ↑(f i) t)
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
⊢ HasSum (fun i => ∫ (x : ℝ) in a..b, ↑(f i) x) (∫ (x : ℝ) in a..b, ∑' (i : ι), ↑(f i) x)
apply hasSum_integral_of_dominated_convergence
  (fun i (x : ℝ) => ‖(f i).restrict ↑(⟨uIcc a b, isCompact_uIcc⟩ : Compacts ℝ)‖)
  (fun i => (map_continuous <| f i).aestronglyMeasurable)
case h_bound
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
i : ι
x : ℝ
hx : x ∈ Ι a b
⊢ ‖↑(f i) x‖ ≤ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
case h_bound
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
⊢ ∀ (n : ι),
    ∀ᵐ (t : ℝ),
      t ∈ Ι a b →
        ‖↑(f n) t‖ ≤ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f n)‖
refine fun i => ae_of_all _ fun x hx => ?_
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
i : ι
x : ℝ
hx : x ∈ Ι a b
⊢ x ∈ ↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }
case h_bound
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
i : ι
x : ℝ
hx : x ∈ Ι a b
⊢ ‖↑(f i) x‖ ≤ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
apply ContinuousMap.norm_coe_le_norm ((f i).restrict _) ⟨x, _⟩
no goals
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
i : ι
x : ℝ
hx : x ∈ Ι a b
⊢ x ∈ ↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }
exact ⟨hx.1.le, hx.2⟩
no goals
case bound_summable
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι a b →
      Summable fun n =>
        ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f n)‖
exact ae_of_all _ fun x _ => hf_sum
no goals
case bound_integrable
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
⊢ IntervalIntegrable
    (fun t =>
      ∑' (n : ι), ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f n)‖)
    volume a b
exact intervalIntegrable_const
case h_lim
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x : ℝ
hx : x ∈ Ι a b
⊢ Summable fun n => ↑(f n) x
case h_lim
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
⊢ ∀ᵐ (t : ℝ), t ∈ Ι a b → HasSum (fun n => ↑(f n) t) (∑' (i : ι), ↑(f i) t)
refine ae_of_all _ fun x hx => Summable.hasSum ?_
case h_lim.refine_2
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x✝ : ℝ
hx : x✝ ∈ Ι a b
x : { x // x ∈ { carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) } } :=
  { val := x✝, property := ?h_lim.refine_1 }
⊢ Summable fun n => ↑(f n) x✝

case h_lim.refine_1
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x : ℝ
hx : x ∈ Ι a b
⊢ x ∈ { carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }
case h_lim
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x : ℝ
hx : x ∈ Ι a b
⊢ Summable fun n => ↑(f n) x
let x : (⟨uIcc a b, isCompact_uIcc⟩ : Compacts ℝ) := ⟨x, ?_⟩
case h_lim.refine_1
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x : ℝ
hx : x ∈ Ι a b
⊢ x ∈ { carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }

case h_lim.refine_2
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x✝ : ℝ
hx : x✝ ∈ Ι a b
x : { x // x ∈ { carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) } } :=
  { val := x✝, property := ?h_lim.refine_1 }
⊢ Summable fun n => ↑(f n) x✝
case h_lim.refine_2
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x✝ : ℝ
hx : x✝ ∈ Ι a b
x : { x // x ∈ { carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) } } :=
  { val := x✝, property := ?h_lim.refine_1 }
⊢ Summable fun n => ↑(f n) x✝

case h_lim.refine_1
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x : ℝ
hx : x ∈ Ι a b
⊢ x ∈ { carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }
swap
case h_lim.refine_2
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x✝ : ℝ
hx : x✝ ∈ Ι a b
x : { x // x ∈ { carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) } } :=
  { val := x✝, property := (_ : a ⊓ b ≤ x✝ ∧ x✝ ≤ a ⊔ b) }
⊢ Summable fun n => ↑(f n) x✝
case h_lim.refine_1
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x : ℝ
hx : x ∈ Ι a b
⊢ x ∈ { carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }

case h_lim.refine_2
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x✝ : ℝ
hx : x✝ ∈ Ι a b
x : { x // x ∈ { carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) } } :=
  { val := x✝, property := ?h_lim.refine_1 }
⊢ Summable fun n => ↑(f n) x✝
exact ⟨hx.1.le, hx.2⟩
case h_lim.refine_2
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x✝ : ℝ
hx : x✝ ∈ Ι a b
x : { x // x ∈ { carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) } } :=
  { val := x✝, property := (_ : a ⊓ b ≤ x✝ ∧ x✝ ≤ a ⊔ b) }
this :
  Summable fun a_1 => ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f a_1)
⊢ Summable fun n => ↑(f n) x✝
case h_lim.refine_2
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x✝ : ℝ
hx : x✝ ∈ Ι a b
x : { x // x ∈ { carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) } } :=
  { val := x✝, property := (_ : a ⊓ b ≤ x✝ ∧ x✝ ≤ a ⊔ b) }
⊢ Summable fun n => ↑(f n) x✝
have := summable_of_summable_norm hf_sum
no goals
case h_lim.refine_2
ι : Type u_1
𝕜 : Type ?u.17271639
E : Type u_2
F : Type ?u.17271645
A : Type ?u.17271648
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f i)‖
x✝ : ℝ
hx : x✝ ∈ Ι a b
x : { x // x ∈ { carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) } } :=
  { val := x✝, property := (_ : a ⊓ b ≤ x✝ ∧ x✝ ≤ a ⊔ b) }
this :
  Summable fun a_1 => ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := (_ : IsCompact [[a, b]]) }) (f a_1)
⊢ Summable fun n => ↑(f n) x✝
simpa only [Compacts.coe_mk, ContinuousMap.restrict_apply]
  using ContinuousMap.summable_apply this x