α : Type u_1
β : Type ?u.27019
ι : Type ?u.27022
E : Type ?u.27025
F : Type ?u.27028
𝕜 : Type ?u.27031
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ ia, True ∧ ∀ (x_1 : ℕ), x_1 ∈ Set.Ici ia → ↑(nearestPt e x_1) x ∈ ball x ε
α : Type u_1
β : Type ?u.27019
ι : Type ?u.27022
E : Type ?u.27025
F : Type ?u.27028
𝕜 : Type ?u.27031
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
⊢ Tendsto (fun N => ↑(nearestPt e N) x) atTop (𝓝 x)
refine' (atTop_basis.tendsto_iff nhds_basis_eball).2 fun ε hε => _
case intro.intro.intro
α : Type u_1
β : Type ?u.27019
ι : Type ?u.27022
E : Type ?u.27025
F : Type ?u.27028
𝕜 : Type ?u.27031
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist x (e N) < ε
⊢ ∃ ia, True ∧ ∀ (x_1 : ℕ), x_1 ∈ Set.Ici ia → ↑(nearestPt e x_1) x ∈ ball x ε
α : Type u_1
β : Type ?u.27019
ι : Type ?u.27022
E : Type ?u.27025
F : Type ?u.27028
𝕜 : Type ?u.27031
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ ia, True ∧ ∀ (x_1 : ℕ), x_1 ∈ Set.Ici ia → ↑(nearestPt e x_1) x ∈ ball x ε
rcases EMetric.mem_closure_iff.1 hx ε hε with ⟨_, ⟨N, rfl⟩, hN⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.27019
ι : Type ?u.27022
E : Type ?u.27025
F : Type ?u.27028
𝕜 : Type ?u.27031
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist (e N) x < ε
⊢ ∃ ia, True ∧ ∀ (x_1 : ℕ), x_1 ∈ Set.Ici ia → ↑(nearestPt e x_1) x ∈ ball x ε
case intro.intro.intro
α : Type u_1
β : Type ?u.27019
ι : Type ?u.27022
E : Type ?u.27025
F : Type ?u.27028
𝕜 : Type ?u.27031
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist x (e N) < ε
⊢ ∃ ia, True ∧ ∀ (x_1 : ℕ), x_1 ∈ Set.Ici ia → ↑(nearestPt e x_1) x ∈ ball x ε
rw [edist_comm] at hN
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.27019
ι : Type ?u.27022
E : Type ?u.27025
F : Type ?u.27028
𝕜 : Type ?u.27031
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist (e N) x < ε
⊢ ∃ ia, True ∧ ∀ (x_1 : ℕ), x_1 ∈ Set.Ici ia → ↑(nearestPt e x_1) x ∈ ball x ε
exact ⟨N, trivial, fun n hn => (edist_nearestPt_le e x hn).trans_lt hN⟩