theorem Multipliable.tendsto_tprod_one {ι : Type u_1} {α : Type u_2} {β : Type u_3} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {l : Filter ι} {s : ι → Set β} (hf : Multipliable f) (hs : ∀ (b : β), ∀ᶠ (i : ι) in l, b ∉ s i) : Filter.Tendsto (fun (i : ι) => ∏' (b : ↑(s i)), f ↑b) l (nhds 1)

theorem Summable.tendsto_tsum_zero {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {l : Filter ι} {s : ι → Set β} (hf : Summable f) (hs : ∀ (b : β), ∀ᶠ (i : ι) in l, b ∉ s i) : Filter.Tendsto (fun (i : ι) => ∑' (b : ↑(s i)), f ↑b) l (nhds 0)