α✝ : Type ?u.261608
β : Type ?u.261611
γ : Type ?u.261614
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) ≠ ⊤
f_ne_top : ∀ (n : α), f n ≠ ⊤
⊢ Tendsto f cofinite (𝓝 0)
α✝ : Type ?u.261608
β : Type ?u.261611
γ : Type ?u.261614
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 f cofinite (𝓝 0)
have f_ne_top : ∀ n, f n ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top hf
α✝ : Type ?u.261608
β : Type ?u.261611
γ : Type ?u.261614
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) ≠ ⊤
f_ne_top : ∀ (n : α), f n ≠ ⊤
h_f_coe : f = fun n => ↑(ENNReal.toNNReal (f n))
⊢ Tendsto f cofinite (𝓝 0)
α✝ : Type ?u.261608
β : Type ?u.261611
γ : Type ?u.261614
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) ≠ ⊤
f_ne_top : ∀ (n : α), f n ≠ ⊤
⊢ Tendsto f cofinite (𝓝 0)
have h_f_coe : f = fun n => ((f n).toNNReal : ENNReal) :=
  funext fun n => (coe_toNNReal (f_ne_top n)).symm
α✝ : Type ?u.261608
β : Type ?u.261611
γ : Type ?u.261614
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) ≠ ⊤
f_ne_top : ∀ (n : α), f n ≠ ⊤
h_f_coe : f = fun n => ↑(ENNReal.toNNReal (f n))
⊢ Tendsto (fun n => ENNReal.toNNReal (f n)) cofinite (𝓝 0)
α✝ : Type ?u.261608
β : Type ?u.261611
γ : Type ?u.261614
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) ≠ ⊤
f_ne_top : ∀ (n : α), f n ≠ ⊤
h_f_coe : f = fun n => ↑(ENNReal.toNNReal (f n))
⊢ Tendsto f cofinite (𝓝 0)
rw [h_f_coe, ← @coe_zero, tendsto_coe]
no goals
α✝ : Type ?u.261608
β : Type ?u.261611
γ : Type ?u.261614
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) ≠ ⊤
f_ne_top : ∀ (n : α), f n ≠ ⊤
h_f_coe : f = fun n => ↑(ENNReal.toNNReal (f n))
⊢ Tendsto (fun n => ENNReal.toNNReal (f n)) cofinite (𝓝 0)
exact NNReal.tendsto_cofinite_zero_of_summable (summable_toNNReal_of_tsum_ne_top hf)