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 is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree
Statement
Let , let and let be a limit point of both and (Limit point, isolated point, adherent point, derived set, and dense subset of , Intervals of : the nine order-convex forms, nondegeneracy, and length), so that both one-sided limits at are well posed (The left and right limits of at , as limits of the restrictions of to and ). Then is a limit point of , and for every :
(The - limit of at a limit point of ). Consequently the limit of at exists if and only if both one-sided limits exist and are equal, and in that case
The hypothesis on both sides is what makes the statement an equivalence. If is a limit point of only one of the two sets — as is for — 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 at , as limits of the restrictions of to and ).
Facts & Assumptions
Given: A set , a function , a real that is a limit point of both and , and a real (Limit point, isolated point, adherent point, derived set, and dense subset of , Intervals of : the nine order-convex forms, nondegeneracy, and length, The left and right limits of at , as limits of the restrictions of to and ).
The limit condition (The - limit of at a limit point of ): means that for every real there is a real such that every in the domain of with satisfies .
Limit point: is a limit point of when for every real there is with (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ).
Intervals: and (Intervals of : the nine order-convex forms, nondegeneracy, and length).
Absolute value and order: exactly when ; the order is total, so every satisfies or ; and is equivalent to for and to for (Basic properties of the absolute value, Ordered field). Of two positive reals the smaller is positive.
Restriction: if has as a limit point and , then (claim 2 of The limit at depends only on the restriction of to a punctured neighbourhood of , and passes to any subset of the domain having as a limit point).
One-sided limits are by definition the limits of the restrictions and at (The left and right limits of at , as limits of the restrictions of to and ).
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 and to it makes each one-sided limit a single real, and applied to it does the same for the two-sided limit.
Proof
is a limit point of : it is one of by hypothesis, and , so every point of found in a punctured neighbourhood of is a point of there.
For the condition says exactly , and then or , that is or ; moreover for the condition reads and for it reads .
Suppose . Both and are subsets of having as a limit point, so [L5] gives and , which by [L6] is exactly and .
Suppose conversely that both one-sided limits equal , and let be an arbitrary real. By [L6] and [L1] fix reals such that every with and every with satisfies ; let be the smaller of the two. Every with lies in or in by step 1.2, and in either case . As was arbitrary, .
The displayed equivalence is steps 2.1 and 2.2. For the consequence: if the limit of at exists, say with value , then step 2.1 gives that both one-sided limits exist with the same value , so they agree; and if both one-sided limits exist and are equal, to the common value , then step 2.2 gives that the limit of at exists and equals . Each of the three symbols denotes a single real by [L7], so the three are equal.
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 depends only on the restriction of to a punctured neighbourhood of , and passes to any subset of the domain having as a limit point; the converse has to glue two estimates, and the gluing is legitimate precisely because every point of other than lies strictly on one side of , 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 , 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
- 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)$
- 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}$
- The $\varepsilon$-neighbourhood and the punctured $\varepsilon$-neighbourhood of a point of $\mathbb{R}$
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- 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
- At a limit point of the domain a function has at most one limit
- Basic properties of the absolute value
- Ordered field
Used by
- A function differentiable on [0,1] whose derivative is unbounded, hence not Riemann integrable Counterexample
- The sign function is Riemann integrable on [-1,1] and has no primitive there Counterexample
- x ↦ |x| is continuous everywhere and not differentiable at 0: the difference quotient equals 1 on the right and -1 on the left, so the two one-sided limits differ Counterexample
- Discontinuity of f at a point of its domain, and its classification: removable discontinuity, jump discontinuity and essential discontinuity, equivalently Rudin's discontinuities of the first and of the second kind Definition
- The sign function has both one-sided limits at 0 and no two-sided limit Example
- FALSE: for every integrable f on [a,b], the integral function F(x)=∫ₐˣ f satisfies F' = f on [a,b] False statement
- A monotone function on an interval has no discontinuity of the second kind: at every point both relevant one-sided limits exist, and an interior point c is a discontinuity exactly when lim_x → c⁻ f(x) < lim_x → c⁺ f(x) Theorem
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
- 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)