∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
  0 < p.toReal → ∀ {C : ℝ}, 0 ≤ C → ∀ {f : ↥(lp E p)}, ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal → ‖f‖ ≤ C