case intro
α✝ : Type ?u.262957
β : Type ?u.262960
γ : Type ?u.262963
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α✝ → ℝ≥0∞
α : Type u_1
f : α → ℝ≥0
hf : (∑' (x : α), (fun i => ↑(f i)) x) ≠ ⊤
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), (fun i => ↑(f i)) ↑b) atTop (𝓝 0)
α✝ : Type ?u.262957
β : Type ?u.262960
γ : Type ?u.262963
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α✝ → ℝ≥0∞
α : Type u_1
f : α → ℝ≥0∞
hf : (∑' (x : α), f x) ≠ ⊤
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop (𝓝 0)
lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hf
case h.e'_3.h
α✝ : Type ?u.262957
β : Type ?u.262960
γ : Type ?u.262963
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α✝ → ℝ≥0∞
α : Type u_1
f : α → ℝ≥0
hf : (∑' (x : α), (fun i => ↑(f i)) x) ≠ ⊤
x✝ : Finset α
⊢ (∑' (b : { x // ¬x ∈ x✝ }), (fun i => ↑(f i)) ↑b) = ↑(∑' (b : { x // ¬x ∈ x✝ }), f ↑b)
case intro
α✝ : Type ?u.262957
β : Type ?u.262960
γ : Type ?u.262963
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α✝ → ℝ≥0∞
α : Type u_1
f : α → ℝ≥0
hf : (∑' (x : α), (fun i => ↑(f i)) x) ≠ ⊤
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), (fun i => ↑(f i)) ↑b) atTop (𝓝 0)
convert ENNReal.tendsto_coe.2 (NNReal.tendsto_tsum_compl_atTop_zero f)
case h.e'_3.h
α✝ : Type ?u.262957
β : Type ?u.262960
γ : Type ?u.262963
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α✝ → ℝ≥0∞
α : Type u_1
f : α → ℝ≥0
hf : (∑' (x : α), (fun i => ↑(f i)) x) ≠ ⊤
x✝ : Finset α
⊢ Summable fun b => f ↑b
case h.e'_3.h
α✝ : Type ?u.262957
β : Type ?u.262960
γ : Type ?u.262963
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α✝ → ℝ≥0∞
α : Type u_1
f : α → ℝ≥0
hf : (∑' (x : α), (fun i => ↑(f i)) x) ≠ ⊤
x✝ : Finset α
⊢ (∑' (b : { x // ¬x ∈ x✝ }), (fun i => ↑(f i)) ↑b) = ↑(∑' (b : { x // ¬x ∈ x✝ }), f ↑b)
rw [ENNReal.coe_tsum]
no goals
case h.e'_3.h
α✝ : Type ?u.262957
β : Type ?u.262960
γ : Type ?u.262963
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α✝ → ℝ≥0∞
α : Type u_1
f : α → ℝ≥0
hf : (∑' (x : α), (fun i => ↑(f i)) x) ≠ ⊤
x✝ : Finset α
⊢ Summable fun b => f ↑b
exact NNReal.summable_comp_injective (tsum_coe_ne_top_iff_summable.1 hf) Subtype.coe_injective