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.
The - limit of at a limit point of
Definition
Throughout, is the complete ordered field (Complete ordered field (least-upper-bound property)) with its order and absolute value (Order on the reals).
Let , let , let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ), and let . We say that tends to as tends to , and write
when
where and range over the positive reals.
In the language of neighbourhoods (The -neighbourhood and the punctured -neighbourhood of a point of ) the condition reads: for every real there is a real with
being the punctured -neighbourhood of and the open interval of Intervals of : the nine order-convex forms, nondegeneracy, and length. The two forms agree because says exactly , and says exactly .
Three features of this definition are load bearing, not decoration.
-
is required to be a limit point of . By Limit point, isolated point, adherent point, derived set, and dense subset of that says every punctured neighbourhood of meets , so for every the set over which the implication quantifies is nonempty. Drop the requirement and the implication can be satisfied vacuously by every real at once, which is exactly what FALSE: a function has at most one limit at every point of its domain, isolated points included records. At a point of that is not a limit point of — an isolated point — the symbol is therefore not defined in this library.
-
is not required. A limit point of need not belong to (Limit point, isolated point, adherent point, derived set, and dense subset of ), and the definition never evaluates at . This is what allows a limit to be taken at a point where the function is not defined at all, as at for .
-
The value , when it exists, is irrelevant. The hypothesis excludes from the quantifier, so changing at the single point changes nothing. Equality of the limit with the value is an extra condition, not a consequence: FALSE: whenever both sides exist.
The notation presumes uniqueness. Writing treats
the left-hand side as a name for a single real number, which is legitimate only
because at a limit point at most one can satisfy the displayed condition.
That obligation is discharged by At a limit point of the domain a function has at most one limit ↗, recorded in this
item's justified_by. As with (Conventions: , unbounded sets, and the extended reals) and
(A sequence has at most one limit), the symbol is written only for a function
already known to have a limit at .
Real and rational define the same relation. Above, and range over the positive reals. Restricting either quantifier to the positive rationals gives the same relation: every positive rational is a positive real, and below every positive real lies a positive rational (The rationals embed densely in the reals), so an -condition verified for all positive rationals is verified for an arbitrary positive real by running it at a rational with , and a produced as a real may be shrunk to a rational one below it. This is the passage sanctioned in the remarks of Sequences of reals: bounded, eventually, frequently, tails, subsequences, and it is what lets this definition be compared with Limits and Cauchy sequences of reals, whose is rational, in Heine criterion: iff for every sequence in converging to .
Remarks
-
Terminology. Limit point here is a property of the set and the point , in the sense of Limit point, isolated point, adherent point, derived set, and dense subset of ; it has nothing to do with subsequential limits (Subsequential limit of a real sequence, and the subsequential limit set), and the distinction is the one that item records.
-
Why the punctured condition, and not . With the unpunctured condition the definition would force to be defined at and would force for every , that is, . The resulting notion is continuity at , a strictly stronger condition, and conflating the two is the error catalogued in FALSE: whenever both sides exist.
-
One-sided and infinite variants. Restricting the domain to one side of gives the one-sided limits of The left and right limits of at , as limits of the restrictions of to and ; replacing the conditions on or on by unboundedness conditions gives the limits at and to infinity of Limits at and , and infinite limits at a point. Both are built on this definition rather than beside it.
Depends on
Limit point, isolated point, adherent point, derived set, and dense subset of
The -neighbourhood and the punctured -neighbourhood of a point of
Intervals of : the nine order-convex forms, nondegeneracy, and length
Order on the reals
Complete ordered field (least-upper-bound property)
Basic properties of the absolute value
The rationals embed densely in the reals