no goals
ι : Type u_1
α : Type ?u.23601
E : Type u_2
F : Type ?u.23607
inst✝² : SeminormedAddCommGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ≥0
hg : Summable g
h : ∀ (i : ι), ‖f i‖₊ ≤ g i
i : ι
⊢ ‖f i‖ ≤ (fun i => ↑(g i)) i
exact_mod_cast h i