TheoremStatement: Literature-sourcedProof: AI-generatedprecheck 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.

If $c$ is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree

Statement

Let $A \subseteq R$ , let $f : A \to R$ and let $c \in R$ be a limit point of both $A^{-} = A \cap (- \infty, c)$ and $A^{+} = A \cap (c, \infty)$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), so that both one-sided limits at $c$ are well posed (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)$ ). Then $c$ is a limit point of $A$ , and for every $L \in R$ :

$\lim_{x \to c} f (x) = L ⟺ \lim_{x \to c^{-}} f (x) = L and \lim_{x \to c^{+}} f (x) = L$

(The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ). Consequently the limit of $f$ at $c$ exists if and only if both one-sided limits exist and are equal, and in that case

$\lim_{x \to c} f (x) = \lim_{x \to c^{-}} f (x) = \lim_{x \to c^{+}} f (x) .$

The hypothesis on both sides is what makes the statement an equivalence. If $c$ is a limit point of only one of the two sets — as $1$ is for ${0} \cup [1, 2]$ — then the one-sided limit on that side and the two-sided limit are the same condition, and the symbol on the other side is not defined at all (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)$ ).

Facts & Assumptions

Given: A set $A \subseteq R$ , a function $f : A \to R$ , a real $c$ that is a limit point of both $A^{-} = A \cap (- \infty, c)$ and $A^{+} = A \cap (c, \infty)$ , and a real $L$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, 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)$ ).

[L1]

The limit condition (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ): $\lim_{x \to c} h (x) = L$ means that for every real $ε > 0$ there is a real $δ > 0$ such that every $x$ in the domain of $h$ with $0 < ∣ x - c ∣ < δ$ satisfies $∣ h (x) - L ∣ < ε$ .

[L2]

Limit point: $c$ is a limit point of $S$ when for every real $δ > 0$ there is $x \in S$ with $0 < ∣ x - c ∣ < δ$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

[L3]

Intervals: $A^{-} = {x \in A : x < c}$ and $A^{+} = {x \in A : x > c}$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L4]

Absolute value and order: $∣ x - c ∣ = 0$ exactly when $x = c$ ; the order is total, so every $x \neq c$ satisfies $x < c$ or $x > c$ ; and $0 < ∣ x - c ∣ < δ$ is equivalent to $c - δ < x < c$ for $x < c$ and to $c < x < c + δ$ for $x > c$ (Basic properties of the absolute value, Ordered field). Of two positive reals the smaller is positive.

[L5]

Restriction: if $B \subseteq A$ has $c$ as a limit point and $\lim_{x \to c} f (x) = L$ , then $\lim_{x \to c} f ∣_{B} (x) = L$ (claim 2 of The limit at $c$ depends only on the restriction of $f$ to a punctured neighbourhood of $c$ , and passes to any subset of the domain having $c$ as a limit point).

[L6]

One-sided limits are by definition the limits of the restrictions $f ∣_{A^{-}}$ and $f ∣_{A^{+}}$ at $c$ (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)$ ).

[L7]

At a limit point of its domain a function has at most one limit (At a limit point of the domain a function has at most one limit); applied to $f ∣_{A^{-}}$ and to $f ∣_{A^{+}}$ it makes each one-sided limit a single real, and applied to $f$ it does the same for the two-sided limit.

Proof

technique · direct

1.1

$c$ is a limit point of $A$ : it is one of $A^{+}$ by hypothesis, and $A^{+} \subseteq A$ , so every point of $A^{+}$ found in a punctured neighbourhood of $c$ is a point of $A$ there.

L2L3

1.2

For $x \in A$ the condition $0 < ∣ x - c ∣$ says exactly $x \neq c$ , and then $x < c$ or $x > c$ , that is $x \in A^{-}$ or $x \in A^{+}$ ; moreover for $x \in A^{-}$ the condition $0 < ∣ x - c ∣ < δ$ reads $c - δ < x < c$ and for $x \in A^{+}$ it reads $c < x < c + δ$ .

L3L4

2.1

Suppose $\lim_{x \to c} f (x) = L$ . Both $A^{-}$ and $A^{+}$ are subsets of $A$ having $c$ as a limit point, so [L5] gives $\lim_{x \to c} f ∣_{A^{-}} (x) = L$ and $\lim_{x \to c} f ∣_{A^{+}} (x) = L$ , which by [L6] is exactly $\lim_{x \to c^{-}} f (x) = L$ and $\lim_{x \to c^{+}} f (x) = L$ .

step 1.1step 1.2L5L6

2.2

Suppose conversely that both one-sided limits equal $L$ , and let $ε > 0$ be an arbitrary real. By [L6] and [L1] fix reals $δ_{1}, δ_{2} > 0$ such that every $x \in A^{-}$ with $0 < ∣ x - c ∣ < δ_{1}$ and every $x \in A^{+}$ with $0 < ∣ x - c ∣ < δ_{2}$ satisfies $∣ f (x) - L ∣ < ε$ ; let $δ$ be the smaller of the two. Every $x \in A$ with $0 < ∣ x - c ∣ < δ$ lies in $A^{-}$ or in $A^{+}$ by step 1.2, and in either case $∣ f (x) - L ∣ < ε$ . As $ε$ was arbitrary, $\lim_{x \to c} f (x) = L$ .

step 1.2L1L4L6choose

3.1

The displayed equivalence is steps 2.1 and 2.2. For the consequence: if the limit of $f$ at $c$ exists, say with value $L$ , then step 2.1 gives that both one-sided limits exist with the same value $L$ , so they agree; and if both one-sided limits exist and are equal, to the common value $L$ , then step 2.2 gives that the limit of $f$ at $c$ exists and equals $L$ . Each of the three symbols denotes a single real by [L7], so the three are equal.

step 2.1step 2.2L7∎

Remarks

The two directions are not symmetric in difficulty. From the two-sided limit to the one-sided ones is pure restriction, The limit at $c$ depends only on the restriction of $f$ to a punctured neighbourhood of $c$ , and passes to any subset of the domain having $c$ as a limit point; the converse has to glue two estimates, and the gluing is legitimate precisely because every point of $A$ other than $c$ lies strictly on one side of $c$ , which is the totality of the order.
The typical failure is a function whose two one-sided limits exist and differ: the sign function at $0$ , on the companion page. Then the two-sided limit cannot exist, since by step 2.1 it would force both one-sided values to equal it.
A function may also have no two-sided limit for a different reason, namely that a one-sided limit fails to exist rather than that the two disagree. The theorem covers that case too, since its right-hand side asserts the existence of both one-sided values, so its failure on one side alone already blocks the two-sided limit. The companion page exhibits both patterns.

Depends on

Used by

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. Lebl, Basic Analysis I, §3.1: Limits of functions (standard reference, not scraped)
One-sided limit (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §9.3 (standard reference, not scraped)

If cc is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree