α : Type u_2
β : Type ?u.775371
γ : Type ?u.775374
δ : Type ?u.775377
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
⊢ e ∈ Filter.map f cofinite
α : Type u_2
β : Type ?u.775371
γ : Type ?u.775374
δ : Type ?u.775377
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
intro e he
α : Type u_2
β : Type ?u.775371
γ : Type ?u.775374
δ : Type ?u.775377
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
⊢ f ⁻¹' e ∈ cofinite
α : Type u_2
β : Type ?u.775371
γ : Type ?u.775374
δ : Type ?u.775377
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
⊢ e ∈ Filter.map f cofinite
rw [Filter.mem_map]
case intro
α : Type u_2
β : Type ?u.775371
γ : Type ?u.775374
δ : Type ?u.775377
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 : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
⊢ f ⁻¹' e ∈ cofinite
α : Type u_2
β : Type ?u.775371
γ : Type ?u.775374
δ : Type ?u.775377
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f : α → G
hf : Summable f
e : Set G
he : e ∈ 𝓝 0
⊢ f ⁻¹' e ∈ cofinite
rcases hf.vanishing he with ⟨s, hs⟩
case intro
α : Type u_2
β : Type ?u.775371
γ : Type ?u.775374
δ : Type ?u.775377
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 : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
x : α
hx : ¬x ∈ s
⊢ f x ∈ e
case intro
α : Type u_2
β : Type ?u.775371
γ : Type ?u.775374
δ : Type ?u.775377
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 : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
⊢ f ⁻¹' e ∈ cofinite
refine' s.eventually_cofinite_nmem.mono fun x hx => _
no goals
case intro
α : Type u_2
β : Type ?u.775371
γ : Type ?u.775374
δ : Type ?u.775377
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 : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∑ k in t, f k ∈ e
x : α
hx : ¬x ∈ s
⊢ f x ∈ e
simpa using hs {x} (disjoint_singleton_left.2 hx)