case intro
α : Type ?u.305098
β : Type ?u.305101
γ : Type ?u.305104
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
fi : Filter ι
x : ℝ≥0∞
hx : x ≠ ⊤
f : ι → ℝ≥0
⊢ Tendsto (fun n => ENNReal.toReal ((fun i => ↑(f i)) n)) fi (𝓝 (ENNReal.toReal x)) ↔ Tendsto (fun i => ↑(f i)) fi (𝓝 x)
α : Type ?u.305098
β : Type ?u.305101
γ : Type ?u.305104
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
x : ℝ≥0∞
hx : x ≠ ⊤
⊢ Tendsto (fun n => ENNReal.toReal (f n)) fi (𝓝 (ENNReal.toReal x)) ↔ Tendsto f fi (𝓝 x)
lift f to ι → ℝ≥0 using hf
case intro.intro
α : Type ?u.305098
β : Type ?u.305101
γ : Type ?u.305104
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
fi : Filter ι
f : ι → ℝ≥0
x : ℝ≥0
⊢ Tendsto (fun n => ENNReal.toReal ((fun i => ↑(f i)) n)) fi (𝓝 (ENNReal.toReal ↑x)) ↔
    Tendsto (fun i => ↑(f i)) fi (𝓝 ↑x)
case intro
α : Type ?u.305098
β : Type ?u.305101
γ : Type ?u.305104
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
fi : Filter ι
x : ℝ≥0∞
hx : x ≠ ⊤
f : ι → ℝ≥0
⊢ Tendsto (fun n => ENNReal.toReal ((fun i => ↑(f i)) n)) fi (𝓝 (ENNReal.toReal x)) ↔ Tendsto (fun i => ↑(f i)) fi (𝓝 x)
lift x to ℝ≥0 using hx
no goals
case intro.intro
α : Type ?u.305098
β : Type ?u.305101
γ : Type ?u.305104
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
fi : Filter ι
f : ι → ℝ≥0
x : ℝ≥0
⊢ Tendsto (fun n => ENNReal.toReal ((fun i => ↑(f i)) n)) fi (𝓝 (ENNReal.toReal ↑x)) ↔
    Tendsto (fun i => ↑(f i)) fi (𝓝 ↑x)
simp [tendsto_coe]