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.
Limits at and , and infinite limits at a point
Definition
Throughout, and are abbreviations and not real numbers, exactly as in Intervals of : the nine order-convex forms, nondegeneracy, and length and Divergence to and to . Every phrase below is a single abbreviation for a displayed condition on reals, and no arithmetic is ever performed with the symbols.
Limits at . Let be not bounded above (Lower bound, bounded below, bounded set), let and let . We write
when for every real there is a real such that
Limits at . Let be not bounded below. We write when for every real there is a real with for every with .
Why unboundedness is required. It plays exactly the role the limit-point condition plays in The - limit of at a limit point of . Saying that is not bounded above says that no real is an upper bound of , that is, that for every real there is with (Lower bound, bounded below, bounded set, Complete ordered field (least-upper-bound property)); so the set over which the condition quantifies is never empty and the condition is never vacuous. Without the hypothesis every real would satisfy it and the notation would not denote.
Uniqueness, proved here. Suppose is not bounded above and and with . Then (Basic properties of the absolute value), so (The multiplicative identity is positive, Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication). Choose reals witnessing the two conditions at this and let be the larger of them, the order being total. Since is not bounded above there is with , hence with and , and then
(The triangle inequality, Basic properties of the absolute value, Order is preserved by adding a constant and by adding inequalities), which trichotomy forbids. So , and the notation denotes a single real. The same four lines, with the inequalities on reversed, give uniqueness at .
Infinite limits at a point. Let , let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ) and let . We write
when for every real there is a real such that for every with ; and as when for every real there is a real with for every such .
This library does not write . The right-hand side would not be an element of , and writing the equation would silently move the discussion into the extended real line, a structure that is not a field. That is the convention already fixed by Divergence to and to for sequences and by Conventions: , unbounded sets, and the extended reals for suprema, and it is kept here. In particular none of the rules of Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero may be applied to a function tending to .
Combined forms. Let be not bounded above and . We write as when for every real there is a real with for every with . The other forms are obtained the same way, by pairing one of the two conditions on (unbounded above, unbounded below) with one of the two conditions on (above every real, below every real); each is again a single abbreviation for the displayed condition, and none of them is an equation.
Remarks
-
These are the same definition with a different notion of "near". In The - limit of at a limit point of the sets shrink to ; here the sets shrink towards being unbounded above. The limit-point hypothesis and the unboundedness hypothesis play the same role: each says the relevant sets are never empty.
-
One-sided infinite limits. Combining this definition with The left and right limits of at , as limits of the restrictions of to and gives, for instance, as , meaning as for the restriction of to , provided is a limit point of that set. Nothing new has to be defined.
-
The extended reals are not needed on these pages. The extended line of The extended real line , its order, and the arithmetic that is left undefined exists in this library and is the right home for ; it is deliberately not used here, because every statement above is a statement about reals and quantifiers, and introducing a second ordered structure would oblige every later algebraic step to say which structure it is working in.
Depends on
- 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}$
- Divergence to $+\infty$ and to $-\infty$
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Lower bound, bounded below, bounded set
- Complete ordered field (least-upper-bound property)
- Basic properties of the absolute value
- The triangle inequality
- Order is preserved by adding a constant and by adding inequalities
- Sign rules for products and monotonicity of multiplication
- Inverses of positives are positive, and reciprocation reverses order
- The multiplicative identity is positive
Used by
- Abel's test for improper integrals Corollary
- Limit comparison for positive improper integrals Corollary
- Cauchy principal values at a finite singularity and on the real line Definition
- Improper integrals over unbounded intervals Definition
- (3x² - 1)/(x² + x) → 3 as x → +∞ Example
- A Dirichlet-type transfer criterion for divergence Theorem
- Dirichlet's test for improper integrals Theorem
- Frullani's formula with its proper integral factor Theorem
- L'Hôpital's rule for the ∞/∞ form at finite or infinite, one-sided endpoints Theorem
- L'Hôpital's rule for the 0/0 form at finite or infinite, one-sided endpoints Theorem
- Linearity of convergent improper integrals Theorem
- The exponential dominates every fixed nonnegative integer power at +∞ Theorem
- The exponential tends to +∞ at +∞ and to 0 at -∞ Theorem
- The improper p-test for rational exponents Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 41 results over 12 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
- Limit of a function (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 4 (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §3.5 (standard reference, not scraped)