Alphabeta Math
TheoremStatement: 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.

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

Statement

Let ARA \subseteq \mathbb{R}, let f:ARf : A \to \mathbb{R} and let cRc \in \mathbb{R} be a limit point of both A=A(,c)A^{-} = A \cap (-\infty, c) and A+=A(c,)A^{+} = A \cap (c, \infty) (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length), so that both one-sided limits at cc are well posed (The left and right limits of ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty)). Then cc is a limit point of AA, and for every LRL \in \mathbb{R}:

limxcf(x)=Llimxcf(x)=L  and  limxc+f(x)=L\lim_{x \to c} f(x) = L \quad \Longleftrightarrow \quad \lim_{x \to c^{-}} f(x) = L \ \text{ and } \ \lim_{x \to c^{+}} f(x) = L

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

limxcf(x)  =  limxcf(x)  =  limxc+f(x).\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 cc is a limit point of only one of the two sets — as 11 is for {0}[1,2]\{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 ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty)).

Facts & Assumptions

Given: A set ARA \subseteq \mathbb{R}, a function f:ARf : A \to \mathbb{R}, a real cc that is a limit point of both A=A(,c)A^{-} = A \cap (-\infty, c) and A+=A(c,)A^{+} = A \cap (c, \infty), and a real LL (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length, The left and right limits of ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty)).

[L1]

The limit condition (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA): limxch(x)=L\lim_{x \to c} h(x) = L means that for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xx in the domain of hh with 0<xc<δ0 < |x - c| < \delta satisfies h(x)L<ε|h(x) - L| < \varepsilon.

[L2]

Limit point: cc is a limit point of SS when for every real δ>0\delta > 0 there is xSx \in S with 0<xc<δ0 < |x - c| < \delta (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L3]

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

[L4]

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

[L5]

Restriction: if BAB \subseteq A has cc as a limit point and limxcf(x)=L\lim_{x \to c} f(x) = L, then limxcfB(x)=L\lim_{x \to c} f|_B(x) = L (claim 2 of The limit at cc depends only on the restriction of ff to a punctured neighbourhood of cc, and passes to any subset of the domain having cc as a limit point).

[L6]

One-sided limits are by definition the limits of the restrictions fAf|_{A^{-}} and fA+f|_{A^{+}} at cc (The left and right limits of ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)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 fAf|_{A^{-}} and to fA+f|_{A^{+}} it makes each one-sided limit a single real, and applied to ff it does the same for the two-sided limit.

Proof

technique · direct
1.1

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

L2L3
1.2

For xAx \in A the condition 0<xc0 < |x - c| says exactly xcx \ne c, and then x<cx < c or x>cx > c, that is xAx \in A^{-} or xA+x \in A^{+}; moreover for xAx \in A^{-} the condition 0<xc<δ0 < |x - c| < \delta reads cδ<x<cc - \delta < x < c and for xA+x \in A^{+} it reads c<x<c+δc < x < c + \delta.

L3L4
2.1

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

step 1.1step 1.2L5L6
2.2

Suppose conversely that both one-sided limits equal LL, and let ε>0\varepsilon > 0 be an arbitrary real. By [L6] and [L1] fix reals δ1,δ2>0\delta_1, \delta_2 > 0 such that every xAx \in A^{-} with 0<xc<δ10 < |x - c| < \delta_1 and every xA+x \in A^{+} with 0<xc<δ20 < |x - c| < \delta_2 satisfies f(x)L<ε|f(x) - L| < \varepsilon; let δ\delta be the smaller of the two. Every xAx \in A with 0<xc<δ0 < |x - c| < \delta lies in AA^{-} or in A+A^{+} by step 1.2, and in either case f(x)L<ε|f(x) - L| < \varepsilon. As ε\varepsilon was arbitrary, limxcf(x)=L\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 ff at cc exists, say with value LL, then step 2.1 gives that both one-sided limits exist with the same value LL, so they agree; and if both one-sided limits exist and are equal, to the common value LL, then step 2.2 gives that the limit of ff at cc exists and equals LL. 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 cc depends only on the restriction of ff to a punctured neighbourhood of cc, and passes to any subset of the domain having cc as a limit point; the converse has to glue two estimates, and the gluing is legitimate precisely because every point of AA other than cc lies strictly on one side of cc, 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 00, 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 35 results over 15 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