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 near and and have the same limit at , then so does
Statement
Let , let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ) and let . Suppose there is a real with
and suppose the limits of and of at exist and are equal, say (The - limit of at a limit point of ). Then the limit of at exists, and
This is the one result on this page that produces a limit rather than computing one. No hypothesis whatever is placed on beyond the two inequalities: may be wildly irregular, as on the companion page is, and the theorem still delivers its limit at .
The proof is a direct - argument and uses no choice principle.
Facts & Assumptions
Given: A set , a limit point of , functions , a real with for every satisfying , and a real with and (The - limit of at a limit point of , Limit point, isolated point, adherent point, derived set, and dense subset of ).
The limit condition: for every real there is a real such that every with satisfies , and likewise for (The - limit of at a limit point of ).
Absolute value: for , is equivalent to (Basic properties of the absolute value).
Order arithmetic in : the order is transitive, and mixed chains compose, so gives and gives ; adding a constant to an inequality (Order is preserved by adding a constant and by adding inequalities); of finitely many positive reals the smallest is positive, the order being total (Ordered field). Order is preserved by adding a constant and by adding inequalities states its moves in their STRICT forms only; the non-strict forms used below follow by adjoining the equality case, in which the two sides coincide, the order being total (Ordered field).
Neighbourhoods: , and a smaller radius gives a smaller punctured neighbourhood (The -neighbourhood and the punctured -neighbourhood of a point of ).
Proof
Let be an arbitrary real. By [L1] fix reals such that every with satisfies and every with satisfies ; let be the smallest of , and , so .
Let with . Then gives , and gives , while gives .
Chaining those four inequalities, , hence , that is , that is .
So for every real a real has been produced with for every satisfying : the limit of at exists and equals .
Remarks
-
Where the three hypotheses are spent. The inequality is used only for the lower estimate and only for the upper one; the equality of the two outer limits is what makes the two estimates close on the same number . Drop it and the argument gives only -style information, which this page does not develop.
-
The order hypothesis is local. It is imposed only on , so the theorem is insensitive to the behaviour of the three functions far from , and to their values at ; that is 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 in action.
-
Typical use. To prove that a bounded oscillating factor is killed by a factor tending to : if near then near , and both outer functions tend to . That is exactly how is proved on the companion page.
-
The sequential analogue is The squeeze theorem.
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}$
- The $\varepsilon$-neighbourhood and the punctured $\varepsilon$-neighbourhood of a point of $\mathbb{R}$
- Basic properties of the absolute value
- Order is preserved by adding a constant and by adding inequalities
- Ordered field
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 29 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
- J. Lebl, Basic Analysis I, §3.1: Limits of functions (standard reference, not scraped)
- Squeeze theorem (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)