no goals
α : Type u_3
β : Type u_1
𝕜 : Type ?u.10501
E : Type ?u.10504
F : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
⊢ ContinuousOn (fun x => ∑' (n : α), f n x) s
classical
  refine' (tendstoUniformlyOn_tsum hu hfu).continuousOn (eventually_of_forall _)
  intro t
  exact continuousOn_finset_sum _ fun i _ => hf i
α : Type u_3
β : Type u_1
𝕜 : Type ?u.10501
E : Type ?u.10504
F : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
⊢ ∀ (x : Finset α), ContinuousOn (fun x_1 => ∑ n in x, f n x_1) s
α : Type u_3
β : Type u_1
𝕜 : Type ?u.10501
E : Type ?u.10504
F : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
⊢ ContinuousOn (fun x => ∑' (n : α), f n x) s
refine' (tendstoUniformlyOn_tsum hu hfu).continuousOn (eventually_of_forall _)
α : Type u_3
β : Type u_1
𝕜 : Type ?u.10501
E : Type ?u.10504
F : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
t : Finset α
⊢ ContinuousOn (fun x => ∑ n in t, f n x) s
α : Type u_3
β : Type u_1
𝕜 : Type ?u.10501
E : Type ?u.10504
F : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
⊢ ∀ (x : Finset α), ContinuousOn (fun x_1 => ∑ n in x, f n x_1) s
intro t
no goals
α : Type u_3
β : Type u_1
𝕜 : Type ?u.10501
E : Type ?u.10504
F : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
t : Finset α
⊢ ContinuousOn (fun x => ∑ n in t, f n x) s
exact continuousOn_finset_sum _ fun i _ => hf i