α : Type u_2
β : Type ?u.773378
γ : Type ?u.773381
δ : Type ?u.773384
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
this : UniformSpace G := TopologicalAddGroup.toUniformSpace G
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
α : Type u_2
β : Type ?u.773378
γ : Type ?u.773381
δ : Type ?u.773384
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
letI : UniformSpace G := TopologicalAddGroup.toUniformSpace G
α : Type u_2
β : Type ?u.773378
γ : Type ?u.773381
δ : Type ?u.773384
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G := comm_topologicalAddGroup_is_uniform
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
α : Type u_2
β : Type ?u.773378
γ : Type ?u.773381
δ : Type ?u.773384
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
this : UniformSpace G := TopologicalAddGroup.toUniformSpace G
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
letI : UniformAddGroup G := comm_topologicalAddGroup_is_uniform
case intro
α : Type u_2
β : Type ?u.773378
γ : Type ?u.773381
δ : Type ?u.773384
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
e : Set G
he : e ∈ 𝓝 0
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G := comm_topologicalAddGroup_is_uniform
y : G
hy : HasSum f y
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
α : Type u_2
β : Type ?u.773378
γ : Type ?u.773381
δ : Type ?u.773384
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G := comm_topologicalAddGroup_is_uniform
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
rcases hf with ⟨y, hy⟩
no goals
case intro
α : Type u_2
β : Type ?u.773378
γ : Type ?u.773381
δ : Type ?u.773384
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
e : Set G
he : e ∈ 𝓝 0
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G := comm_topologicalAddGroup_is_uniform
y : G
hy : HasSum f y
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
exact cauchySeq_finset_iff_vanishing.1 hy.cauchySeq e he