α : Type u_1
β : Type u_3
𝕜 : Type ?u.6502
E : Type ?u.6505
F : Type u_2
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x => ∑ n in t, f n x) (fun x => ∑' (n : α), f n x) atTop univ
α : Type u_1
β : Type u_3
𝕜 : Type ?u.6502
E : Type ?u.6505
F : Type u_2
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformly (fun t x => ∑ n in t, f n x) (fun x => ∑' (n : α), f n x) atTop
rw [← tendstoUniformlyOn_univ]
no goals
α : Type u_1
β : Type u_3
𝕜 : Type ?u.6502
E : Type ?u.6505
F : Type u_2
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x => ∑ n in t, f n x) (fun x => ∑' (n : α), f n x) atTop univ
exact tendstoUniformlyOn_tsum hu fun n x _ => hfu n x