Limit_of_Sequence_to_Zero_Distance_Point
Provedlimit-pointslimits-of-sequencesproofwiki
If x is a limit point of a set S of reals, then there exists a sequence in S converging to x.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Limit_of_Sequence_to_Zero_Distance_Point (S : Set ℝ) (x : ℝ) (hx : ∀ ε > 0, ∃ s ∈ S, |s - x| < ε) : ∃ a : ℕ → ℝ, (∀ n, a n ∈ S) ∧ Filter.Tendsto a Filter.atTop (nhds x) := by sorry
Source