case pos
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop (𝓝 0)

case neg
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : ¬Summable f
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop (𝓝 0)
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop (𝓝 0)
by_cases H : Summable f
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
⊢ e ∈ Filter.map (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop (𝓝 0)
intro e he
case pos.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
⊢ e ∈ Filter.map (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
⊢ e ∈ Filter.map (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop
rcases exists_mem_nhds_isClosed_subset he with ⟨o, ho, o_closed, oe⟩
case pos.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
⊢ ∃ a, ∀ (b : Finset β), a ⊆ b → (∑' (b_1 : { x // ¬x ∈ b }), f ↑b_1) ∈ e
case pos.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
⊢ e ∈ Filter.map (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop
simp only [le_eq_subset, Set.mem_preimage, mem_atTop_sets, Filter.mem_map, ge_iff_le]
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
⊢ ∃ a, ∀ (b : Finset β), a ⊆ b → (∑' (b_1 : { x // ¬x ∈ b }), f ↑b_1) ∈ e
case pos.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
⊢ ∃ a, ∀ (b : Finset β), a ⊆ b → (∑' (b_1 : { x // ¬x ∈ b }), f ↑b_1) ∈ e
obtain ⟨s, hs⟩ : ∃ s : Finset β, ∀ t : Finset β, Disjoint t s → (∑ b : β in t, f b) ∈ o :=
  cauchySeq_finset_iff_vanishing.1 (Tendsto.cauchySeq H.hasSum) o ho
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
⊢ (∑' (b : { x // ¬x ∈ a }), f ↑b) ∈ o
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
⊢ ∃ a, ∀ (b : Finset β), a ⊆ b → (∑' (b_1 : { x // ¬x ∈ b }), f ↑b_1) ∈ e
refine' ⟨s, fun a sa => oe _⟩
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
⊢ (∑' (b : { x // ¬x ∈ a }), f ↑b) ∈ o
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
⊢ (∑' (b : { x // ¬x ∈ a }), f ↑b) ∈ o
have A : Summable fun b : { x // x ∉ a } => f b := a.summable_compl_iff.2 H
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
⊢ ∑ b in b, (fun b => f ↑b) b ∈ o
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
⊢ (∑' (b : { x // ¬x ∈ a }), f ↑b) ∈ o
refine' IsClosed.mem_of_tendsto o_closed A.hasSum (eventually_of_forall fun b => _)
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
this : Disjoint (image (fun i => ↑i) b) s
⊢ ∑ b in b, (fun b => f ↑b) b ∈ o
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
⊢ ∑ b in b, (fun b => f ↑b) b ∈ o
have : Disjoint (Finset.image (fun i : { x // x ∉ a } => (i : β)) b) s := by
  refine' disjoint_left.2 fun i hi his => _
  rcases mem_image.1 hi with ⟨i', _, rfl⟩
  exact i'.2 (sa his)
case h.e'_4
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
this : Disjoint (image (fun i => ↑i) b) s
⊢ ∑ b in b, (fun b => f ↑b) b = ∑ b in image (fun i => ↑i) b, f b
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
this : Disjoint (image (fun i => ↑i) b) s
⊢ ∑ b in b, (fun b => f ↑b) b ∈ o
convert hs _ this using 1
case h.e'_4
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
this : Disjoint (image (fun i => ↑i) b) s
⊢ ∀ (x : { x // ¬x ∈ a }), x ∈ b → ∀ (y : { x // ¬x ∈ a }), y ∈ b → ↑x = ↑y → x = y
case h.e'_4
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
this : Disjoint (image (fun i => ↑i) b) s
⊢ ∑ b in b, (fun b => f ↑b) b = ∑ b in image (fun i => ↑i) b, f b
rw [sum_image]
case h.e'_4
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝² a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
this : Disjoint (image (fun i => ↑i) b) s
i : { x // ¬x ∈ a }
a✝¹ : i ∈ b
j : { x // ¬x ∈ a }
a✝ : j ∈ b
hij : ↑i = ↑j
⊢ i = j
case h.e'_4
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
this : Disjoint (image (fun i => ↑i) b) s
⊢ ∀ (x : { x // ¬x ∈ a }), x ∈ b → ∀ (y : { x // ¬x ∈ a }), y ∈ b → ↑x = ↑y → x = y
intro i _ j _ hij
no goals
case h.e'_4
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝² a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
this : Disjoint (image (fun i => ↑i) b) s
i : { x // ¬x ∈ a }
a✝¹ : i ∈ b
j : { x // ¬x ∈ a }
a✝ : j ∈ b
hij : ↑i = ↑j
⊢ i = j
exact Subtype.ext hij
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
i : β
hi : i ∈ image (fun i => ↑i) b
his : i ∈ s
⊢ False
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
⊢ Disjoint (image (fun i => ↑i) b) s
refine' disjoint_left.2 fun i hi his => _
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
i' : { x // ¬x ∈ a }
left✝ : i' ∈ b
hi : ↑i' ∈ image (fun i => ↑i) b
his : ↑i' ∈ s
⊢ False
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
i : β
hi : i ∈ image (fun i => ↑i) b
his : i ∈ s
⊢ False
rcases mem_image.1 hi with ⟨i', _, rfl⟩
no goals
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : β → α
H : Summable f
e : Set α
he : e ∈ 𝓝 0
o : Set α
ho : o ∈ 𝓝 0
o_closed : IsClosed o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ o
a : Finset β
sa : s ⊆ a
A : Summable fun b => f ↑b
b : Finset { x // ¬x ∈ a }
i' : { x // ¬x ∈ a }
left✝ : i' ∈ b
hi : ↑i' ∈ image (fun i => ↑i) b
his : ↑i' ∈ s
⊢ False
exact i'.2 (sa his)
case h.e'_3.h
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : ¬Summable f
x✝ : Finset β
⊢ (∑' (b : { x // ¬x ∈ x✝ }), f ↑b) = 0
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : ¬Summable f
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop (𝓝 0)
convert tendsto_const_nhds (α := α) (β := Finset β) (f := atTop) (a := 0)
case h.e'_3.h.h
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : ¬Summable f
x✝ : Finset β
⊢ ¬Summable fun b => f ↑b
case h.e'_3.h
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : ¬Summable f
x✝ : Finset β
⊢ (∑' (b : { x // ¬x ∈ x✝ }), f ↑b) = 0
apply tsum_eq_zero_of_not_summable
no goals
case h.e'_3.h.h
α : Type u_2
β : Type u_1
γ : Type ?u.676328
δ : Type ?u.676331
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
f : β → α
H : ¬Summable f
x✝ : Finset β
⊢ ¬Summable fun b => f ↑b
rwa [Finset.summable_compl_iff]