case intro
α : Type ?u.26680
β : Type ?u.26683
γ : Type ?u.26686
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0
⊢ Tendsto ENNReal.toNNReal (𝓝 ↑a) (𝓝 (ENNReal.toNNReal ↑a))
α : Type ?u.26680
β : Type ?u.26683
γ : Type ?u.26686
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ Tendsto ENNReal.toNNReal (𝓝 a) (𝓝 (ENNReal.toNNReal a))
lift a to ℝ≥0 using ha
case intro
α : Type ?u.26680
β : Type ?u.26683
γ : Type ?u.26686
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0
⊢ Tendsto (ENNReal.toNNReal ∘ some) (𝓝 a) (𝓝 (ENNReal.toNNReal ↑a))
case intro
α : Type ?u.26680
β : Type ?u.26683
γ : Type ?u.26686
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0
⊢ Tendsto ENNReal.toNNReal (𝓝 ↑a) (𝓝 (ENNReal.toNNReal ↑a))
rw [nhds_coe, tendsto_map'_iff]
no goals
case intro
α : Type ?u.26680
β : Type ?u.26683
γ : Type ?u.26686
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0
⊢ Tendsto (ENNReal.toNNReal ∘ some) (𝓝 a) (𝓝 (ENNReal.toNNReal ↑a))
exact tendsto_id