ι : Type u_2
α : Type ?u.14525
E : Type u_1
F : Type ?u.14531
inst✝² : SeminormedAddCommGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ CauchySeq fun s => ∑ b in s, f b
ι : Type u_2
α : Type ?u.14525
E : Type u_1
F : Type ?u.14531
inst✝² : SeminormedAddCommGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ Summable f
rw [summable_iff_cauchySeq_finset]
no goals
ι : Type u_2
α : Type ?u.14525
E : Type u_1
F : Type ?u.14531
inst✝² : SeminormedAddCommGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ CauchySeq fun s => ∑ b in s, f b
exact cauchySeq_finset_of_norm_bounded g hg h