α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type ?u.332033
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f✝ g✝ : β → α
a a₁ a₂ : α
α' : Type u_1
inst✝¹ : AddCommMonoid α'
inst✝ : TopologicalSpace α'
e : α' → α
hes : Surjective e
h0 : e 0 = 0
f : β → α
g : γ → α'
h : ∀ {a : α'}, HasSum f (e a) ↔ HasSum g a
hg : ¬Summable g
hf : ¬Summable f
⊢ (∑' (b : β), f b) = e (∑' (c : γ), g c)
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type ?u.332033
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f✝ g✝ : β → α
a a₁ a₂ : α
α' : Type u_1
inst✝¹ : AddCommMonoid α'
inst✝ : TopologicalSpace α'
e : α' → α
hes : Surjective e
h0 : e 0 = 0
f : β → α
g : γ → α'
h : ∀ {a : α'}, HasSum f (e a) ↔ HasSum g a
hg : ¬Summable g
⊢ (∑' (b : β), f b) = e (∑' (c : γ), g c)
have hf : ¬Summable f := mt (hes.summable_iff_of_hasSum_iff @h).1 hg
no goals
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type ?u.332033
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f✝ g✝ : β → α
a a₁ a₂ : α
α' : Type u_1
inst✝¹ : AddCommMonoid α'
inst✝ : TopologicalSpace α'
e : α' → α
hes : Surjective e
h0 : e 0 = 0
f : β → α
g : γ → α'
h : ∀ {a : α'}, HasSum f (e a) ↔ HasSum g a
hg : ¬Summable g
hf : ¬Summable f
⊢ (∑' (b : β), f b) = e (∑' (c : γ), g c)
simp [tsum_def, hf, hg, h0]