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 left and right limits of at , as limits of the restrictions of to and
Definition
Let , let and let . Put
(Intervals of : the nine order-convex forms, nondegeneracy, and length), and write and for the restrictions of to those sets.
Right limit. Suppose is a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ). For we write
in the sense of The - limit of at a limit point of . Written out: for every real there is a real such that
Left limit. Suppose is a limit point of . For we write when ; written out, for every real there is a real with for every with .
The written-out forms agree with the definitions. For the two conditions and are the same: gives , so and reads (Basic properties of the absolute value). Symmetrically on the left, where gives .
Well-posedness is inherited, not reproved. A one-sided limit is a limit, namely the limit of a restriction, so:
- Uniqueness. At most one can occur, by At a limit point of the domain a function has at most one limit applied to on the domain (respectively to on ), which is legitimate exactly because was required to be a limit point of that set. This is what makes the notation denote a single real.
- Locality and restriction. Both claims 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 apply verbatim to and .
When the symbols are defined. If is not a limit point of — for instance if contains no point to the right of , or only points bounded away from on that side — then is not defined here, for the reason given in The - limit of at a limit point of : the - condition would be satisfied vacuously by every real at once. The same applies on the left.
Remarks
-
Neither one-sided limit requires , and neither looks at . Both properties are inherited from The - limit of at a limit point of , since : the point belongs to neither nor .
-
The two one-sided limits and the two-sided limit. When is a limit point of both and , the two-sided limit exists exactly when both one-sided limits exist and agree, and then all three coincide: If is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree. When is a limit point of only one of the two sets, that one-sided limit and the two-sided limit are the same condition, again by 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 together with the observation that and that one side have the same points in a small enough punctured neighbourhood of .
-
Notation. Some texts write and for these values. This library writes only and , because the shorter notation looks like an evaluation of and these quantities are not values of : they are defined without reference to , which may not even exist.
Depends on
The - limit of at a limit point of
Limit point, isolated point, adherent point, derived set, and dense subset of
Intervals of : the nine order-convex forms, nondegeneracy, and length
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
At a limit point of the domain a function has at most one limit
Basic properties of the absolute value