α : Type ?u.360325
β : Type u_3
γ : Type u_2
δ : Type u_1
inst✝⁷ : AddCommMonoid α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
inst✝⁴ : ContinuousAdd α
inst✝³ : AddCommMonoid δ
inst✝² : TopologicalSpace δ
inst✝¹ : T3Space δ
inst✝ : ContinuousAdd δ
f : β → γ → δ
h : Summable (uncurry f)
h₁ : ∀ (b : β), Summable (f b)
h₂ : ∀ (c : γ), Summable fun b => f b c
⊢ (∑' (p : γ × β), uncurry f (Prod.swap p)) = ∑' (c : γ × β), uncurry f (↑(Equiv.prodComm γ β) c)
α : Type ?u.360325
β : Type u_3
γ : Type u_2
δ : Type u_1
inst✝⁷ : AddCommMonoid α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
inst✝⁴ : ContinuousAdd α
inst✝³ : AddCommMonoid δ
inst✝² : TopologicalSpace δ
inst✝¹ : T3Space δ
inst✝ : ContinuousAdd δ
f : β → γ → δ
h : Summable (uncurry f)
h₁ : ∀ (b : β), Summable (f b)
h₂ : ∀ (c : γ), Summable fun b => f b c
⊢ (∑' (c : γ) (b : β), f b c) = ∑' (b : β) (c : γ), f b c
erw [← tsum_prod' h h₁, ← tsum_prod' h.prod_symm h₂, ← (Equiv.prodComm γ β).tsum_eq (uncurry f)]
no goals
α : Type ?u.360325
β : Type u_3
γ : Type u_2
δ : Type u_1
inst✝⁷ : AddCommMonoid α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
inst✝⁴ : ContinuousAdd α
inst✝³ : AddCommMonoid δ
inst✝² : TopologicalSpace δ
inst✝¹ : T3Space δ
inst✝ : ContinuousAdd δ
f : β → γ → δ
h : Summable (uncurry f)
h₁ : ∀ (b : β), Summable (f b)
h₂ : ∀ (c : γ), Summable fun b => f b c
⊢ (∑' (p : γ × β), uncurry f (Prod.swap p)) = ∑' (c : γ × β), uncurry f (↑(Equiv.prodComm γ β) c)
rfl