no goals
α : Type u_1
β : Type ?u.799420
γ : Type ?u.799423
δ : Type ?u.799426
ι : Type u_3
π : α → Type u_2
inst✝¹ : (x : α) → AddCommMonoid (π x)
inst✝ : (x : α) → TopologicalSpace (π x)
f : ι → (x : α) → π x
⊢ Summable f ↔ ∀ (x : α), Summable fun i => f i x
simp only [Summable, Pi.hasSum, skolem]