def ContinuousFunctions.IsClusterPoint (S : Set ℝ) (x : ℝ) : Prop

x is a cluster point of S if every punctured neighborhood (x - δ, x + δ) \ {x} of x meets S, i.e. for all δ > 0 there exists y ∈ S with y ≠ x and |y - x| < δ.

theorem ContinuousFunctions.cluster_point_iff_acc_point (S : Set ℝ) (x : ℝ) : IsClusterPoint S x ↔ AccPt x (Filter.principal S)

The elementary ε-δ notion IsClusterPoint S x agrees with Mathlib's topological accumulation point AccPt x (𝓟 S).

def ContinuousFunctions.FunctionConvergesAt (f : ℝ → ℝ) (S : Set ℝ) (c L : ℝ) : Prop

f converges to L at c along S, written informally f(x) → L as x → c, if for every ε > 0 there exists δ > 0 such that for all x ∈ S with 0 < |x - c| < δ one has |f x - L| < ε.

theorem ContinuousFunctions.function_limit_iff_tendsto (f : ℝ → ℝ) (S : Set ℝ) (c L : ℝ) : FunctionConvergesAt f S c L ↔ Filter.Tendsto f (nhdsWithin c (S \ {c})) (nhds L)

The elementary ε-δ definition FunctionConvergesAt f S c L is equivalent to the Mathlib filter statement that f tends to L along the neighborhood filter of c restricted to S \ {c}.

def ContinuousFunctions.RightLimit (f : ℝ → ℝ) (S : Set ℝ) (c L : ℝ) : Prop

The right-hand limit f(x) → L as x → c⁺ along S: for every ε > 0 there exists δ > 0 such that for all x ∈ S with c < x < c + δ one has |f x - L| < ε.

theorem ContinuousFunctions.function_limit_unique (f : ℝ → ℝ) (S : Set ℝ) (c L₁ L₂ : ℝ) (hc : IsClusterPoint S c) (hL₁ : FunctionConvergesAt f S c L₁) (hL₂ : FunctionConvergesAt f S c L₂) : L₁ = L₂

Uniqueness of the function limit: if c is a cluster point of S and f converges both to L₁ and to L₂ at c along S, then L₁ = L₂.