LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

At a limit point of the domain a function has at most one limit

Statement

Let $A \subseteq \mathbb{R}$ , let $f : A \to \mathbb{R}$ , let $c$ be a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$ ) and let $L, L' \in \mathbb{R}$ . If

$\lim_{x \to c} f(x) = L \qquad \text{and} \qquad \lim_{x \to c} f(x) = L'$

(The $\varepsilon$ - $\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$ ), then $L = L'$ .

A function therefore has at most one limit at a limit point of its domain, which is what licenses the notation $\lim_{x \to c} f(x)$ for a single real number. This lemma is recorded in the justified_by field of The $\varepsilon$ - $\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$ for exactly that reason.

The hypothesis that $c$ is a limit point is not removable. At an isolated point of the domain the same $\varepsilon$ - $\delta$ formula is satisfied vacuously by every real at once, which is the content of FALSE: a function has at most one limit at every point of its domain, isolated points included.

Facts & Assumptions

Given: A set $A \subseteq \mathbb{R}$ , a function $f : A \to \mathbb{R}$ , a limit point $c$ of $A$ , and reals $L, L'$ with $\lim_{x \to c} f(x) = L$ and $\lim_{x \to c} f(x) = L'$ (The $\varepsilon$ - $\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$ , Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$ ).

[L1]

The limit condition: for every real $\varepsilon > 0$ there is a real $\delta > 0$ such that every $x \in A$ with $0 < |x - c| < \delta$ satisfies $|f(x) - L| < \varepsilon$ , and likewise with $L'$ in place of $L$ (The $\varepsilon$ - $\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$ ).

[L2]

Limit point: for every real $\delta > 0$ there is $x \in A$ with $0 < |x - c| < \delta$ (Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$ , The $\varepsilon$ -neighbourhood and the punctured $\varepsilon$ -neighbourhood of a point of $\mathbb{R}$ ).

[L3]

Triangle inequality: $|u + v| \le |u| + |v|$ in $\mathbb{R}$ (The triangle inequality).

[L4]

Absolute value: $|u| \ge 0$ ; $|u| = 0$ if and only if $u = 0$ ; and $|-u| = |u|$ (Basic properties of the absolute value).

[L5]

Order arithmetic in $\mathbb{R}$ : trichotomy, so $u \ne 0$ together with $|u| \ge 0$ and $|u| \ne 0$ forces $|u| > 0$ , and $t < t$ is impossible; adding two strict inequalities (Order is preserved by adding a constant and by adding inequalities); $0 < 1$ (The multiplicative identity is positive), hence $2 := 1 + 1 > 0$ and $2^{-1} > 0$ (Inverses of positives are positive, and reciprocation reverses order), so $\eta/2 > 0$ and $(\eta/2) \cdot 2 = \eta$ whenever $\eta > 0$ (Sign rules for products and monotonicity of multiplication, Ordered field); and of two positive reals the smaller is positive, the order being total.

Proof

technique · contradiction

1.1

Suppose, for contradiction, that $L \ne L'$ .

assume-contra

2.1

Then $L - L' \ne 0$ , so $|L - L'| \ne 0$ while $|L - L'| \ge 0$ , and trichotomy gives $|L - L'| > 0$ ; hence $\varepsilon := |L - L'|/2 > 0$ and $2\varepsilon = |L - L'|$ .

step 1.1L4L5

3.1

Applying [L1] twice with this $\varepsilon$ , fix reals $\delta_1 > 0$ and $\delta_2 > 0$ such that every $x \in A$ with $0 < |x - c| < \delta_1$ has $|f(x) - L| < \varepsilon$ and every $x \in A$ with $0 < |x - c| < \delta_2$ has $|f(x) - L'| < \varepsilon$ ; put $\delta$ to be the smaller of $\delta_1$ and $\delta_2$ , so $\delta > 0$ .

step 2.1L1L5choose

4.1

Since $c$ is a limit point of $A$ , fix $x \in A$ with $0 < |x - c| < \delta$ .

step 3.1L2choose

5.1

That $x$ satisfies $0 < |x - c| < \delta_1$ and $0 < |x - c| < \delta_2$ , hence both $|f(x) - L| < \varepsilon$ and $|f(x) - L'| < \varepsilon$ .

step 3.1step 4.1L1

6.1

Therefore $|L - L'| = |(L - f(x)) + (f(x) - L')| \le |L - f(x)| + |f(x) - L'| = |f(x) - L| + |f(x) - L'| < \varepsilon + \varepsilon = 2\varepsilon = |L - L'|$ .

step 5.1L3L4L5

7.1

So $|L - L'| < |L - L'|$ , which trichotomy forbids; the assumption $L \ne L'$ is untenable, and hence $L = L'$ .

step 6.1L5discharge-contradiction∎

Remarks

Where each hypothesis is spent. The limit conditions are used only in step 5.1, and the limit-point hypothesis only in step 4.1, to produce a single point $x$ of the domain near $c$ at which both estimates can be read. Without such a point the two estimates never meet and nothing forces $L = L'$ ; that is the whole mechanism, and it is the reason FALSE: a function has at most one limit at every point of its domain, isolated points included is false.
The sequential analogue is A sequence has at most one limit, proved by the same two-estimates-at-one-index argument. Neither statement uses any choice principle.
One-sided limits inherit this. By The left and right limits of $f$ at $c$ , as limits of the restrictions of $f$ to $A \cap (-\infty, c)$ and $A \cap (c, \infty)$ a one-sided limit is the limit of a restriction of $f$ , so applying this lemma to that restriction gives uniqueness there too; nothing has to be reproved.

Depends on

Used by

Cited to discharge well-definedness by The ε-δ limit lim_x → c f(x) = L of f : A → ℝ at a limit point c of A.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 32 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Lebl, Basic Analysis I, §3.1: Limits of functions (standard reference, not scraped)
Limit of a function (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 4 (standard reference, not scraped)
J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)