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 of Real Functions
1 · Prerequisites
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Countability and Uncountability
- Foundations of the Real Numbers for Analysis
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Relations, Functions, and Quotients
- Sequences and Limits
- Suprema and Infima
- The ZFC Axioms and the Basic Set Constructions
- Topology of ℝ
2 · Summary
Objective. This page defines what it means for a function of a real variable to have a limit at a point, and proves the toolkit that makes the notion usable: uniqueness, locality, the algebra of limits, order preservation, the squeeze theorem, the relation between the two-sided limit and the two one-sided limits, and composition. It is built on the topology of (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ) and on the theory of sequences, and it is the last page before continuity.
The definition, and the three decisions inside it. The - limit of at a limit point of says that when for every real there is a real with for every in the domain satisfying . Three features are load bearing rather than decorative, and two of the three have a false statement on this page attached to them.
- must be a limit point of the domain. That is what keeps the quantified
set nonempty for every , and hence what allows the condition to pin
down. At a limit point of the domain a function has at most one limit then proves that at most one can occur,
which is exactly what licenses the notation, and it is recorded in the
definition's
justified_byfor that reason. Drop the hypothesis and uniqueness fails completely: at an isolated point every real satisfies the formula vacuously, which is FALSE: a function has at most one limit at every point of its domain, isolated points included. So at an isolated point of the domain the symbol is simply not defined here. - need not lie in the domain, so a limit may be taken where the function is not defined.
- The value , when it exists, is invisible, because removes from the quantifier. Equality of limit and value is therefore a hypothesis and not a consequence, which is FALSE: whenever both sides exist; that equality is what continuity at will mean, on the next page of this track.
Locality. 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 proves the two statements that make the limit a local object: changing outside a punctured neighbourhood of changes nothing, and a limit survives restricting the domain to any subset that still has as a limit point. Everything later on this page that shrinks a domain — the one-sided limits, the quotient rule — goes through it.
The two variants. The left and right limits of at , as limits of the restrictions of to and defines as the limit of the restriction of to the points of the domain on one side of , so uniqueness and locality are inherited rather than reproved. Limits at and , and infinite limits at a point defines limits at , where the role of the limit-point hypothesis is played by unboundedness of the domain, and infinite limits at a point. The symbols remain abbreviations and never real numbers: the library does not write , for the reason Divergence to and to already gave for sequences. Uniqueness of the limit at is proved inside that definition.
Choice hygiene, and why it shapes the page. Heine criterion: iff for every sequence in converging to — the Heine criterion — says that if and only if for every sequence in the domain avoiding and converging to . Its two directions do not cost the same. The direction from - to sequences is a theorem of ZF. The converse, as proved here, invokes the axiom of countable choice (The Axiom of Countable Choice ()) exactly once, to pick one bad point from each of countably many nonempty sets — the same use, for the same reason, as in A point lies in the closure of iff some sequence in converges to it, so a subset of is closed iff it is sequentially closed on the prerequisite page. The sequence-to- direction of the Heine criterion uses countable choice for , and where this library records that cost records precisely what is and is not claimed about that: in particular this library does not claim the axiom is necessary, and it warns against the slogan that sequential criteria always need choice, since Sierpiński's theorem on everywhere-sequentially-continuous functions is a theorem of ZF.
The consequence for this page is a deliberate organisation. Everything that can be proved directly from and is proved that way, so the algebra of limits, order preservation, the squeeze theorem and composition are all theorems of ZF. The sequential side is used only where it earns its place: in the criterion itself, and in A function has no limit at as soon as two sequences in tending to give different limits of the values, which needs only the choice-free direction and is the standard way to show that a limit does not exist — two sequences tending to whose image sequences tend to different values, or one whose image sequence does not converge at all.
The toolkit, in the order it is needed. If has a finite limit at then is bounded on some punctured neighbourhood of shows that a function with a limit at is bounded on some punctured neighbourhood of — and only there, which is FALSE: a function with a limit at is bounded on its whole domain. If then on a punctured neighbourhood of ; in particular if then there shows that a nonzero limit forces on a punctured neighbourhood, with the sign of , and that remains a limit point of the set where does not vanish. Those two lemmas are exactly what the product and quotient cases of the next theorem need, which is why they precede it.
Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero then proves that sums, scalar multiples, products and quotients of limits behave as expected, the quotient on the domain where the denominator does not vanish and under the hypothesis that its limit is nonzero. Each claim asserts both that the compound limit exists and what it equals. If on a punctured neighbourhood of then , non-strictly proves that near gives ; the conclusion cannot be sharpened to a strict inequality even from a strict hypothesis, which is FALSE: near implies . If near and and have the same limit at , then so does is the one result here that produces a limit rather than computing one: no hypothesis is placed on the squeezed function at all. If is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree closes the loop with the one-sided limits.
Composition, with the hypothesis that is usually left implicit. Composition of limits holds under either hypothesis: is defined at with value , or avoids on a punctured neighbourhood of is false as usually first stated. The inner limit controls but does not prevent from equalling , and at those arguments the outer limit says nothing, since it never sees . Two hypotheses each close the gap, and either suffices: (i) lies in the outer domain with , which is continuity of at written out; or (ii) avoids the value on a punctured neighbourhood of , which is what makes substitutions such as legitimate. With both dropped the statement is refuted by FALSE: whenever and , whose witness fails (i) and (ii) at once.
One reusable lemma, deliberately placed here. Integer part: for every real there is exactly one integer with proves that every real has exactly one integer with . Existence is the Archimedean property together with the well-ordering of ; uniqueness is the discreteness of . It is the library's first floor item, and it is stated on this page rather than inside an example so that later pages — monotone functions, powers, content — can cite it instead of rebuilding the argument. Its immediate use is on the companion page, where it computes the trigonometry-free oscillator in one line.
The companion page carries the witnesses: polynomials and rational functions, the oscillator and the two examples built on it, the sign function, a limit at computed by a direct estimate, the indicator of , and the counterexample items that work three of the five false statements listed here out in full. Each of the five already carries its own witness, verified in the false statement itself; what the companion page adds, for those three, is the further computation each witness supports.
3 · Logical flowchart
4 · Definitions, theorems and proofs
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.
At a limit point of the domain a function has at most one limit
Statement
Let , let , let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ) and let . If
(The - limit of at a limit point of ), then .
A function therefore has at most one limit at a limit point of its domain,
which is what licenses the notation for a single real
number. This lemma is recorded in the justified_by field of
The - limit of at a limit point of for exactly that reason.
The hypothesis that is a limit point is not removable. At an isolated point of the domain the same - formula is satisfied vacuously by every real at once, which is the content of FALSE: a function has at most one limit at every point of its domain, isolated points included.
Facts & Assumptions
Given: A set , a function , a limit point of , and reals 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 with in place of (The - limit of at a limit point of ).
Limit point: 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 ).
Triangle inequality: in (The triangle inequality).
Absolute value: ; if and only if ; and (Basic properties of the absolute value).
Order arithmetic in : trichotomy, so together with and forces , and is impossible; adding two strict inequalities (Order is preserved by adding a constant and by adding inequalities); (The multiplicative identity is positive), hence and (Inverses of positives are positive, and reciprocation reverses order), so and whenever (Sign rules for products and monotonicity of multiplication, Ordered field); and of two positive reals the smaller is positive, the order being total.
Proof
Suppose, for contradiction, that .
Then , so while , and trichotomy gives ; hence and .
Applying [L1] twice with this , fix reals and such that every with has and every with has ; put to be the smaller of and , so .
Since is a limit point of , fix with .
That satisfies and , hence both and .
Therefore .
So , which trichotomy forbids; the assumption is untenable, and hence .
Remarks
-
Where each hypothesis is spent. The limit conditions are used only in step 5.1, and the limit-point hypothesis only in step 4.1, to produce a single point of the domain near at which both estimates can be read. Without such a point the two estimates never meet and nothing forces ; that is the whole mechanism, and it is the reason FALSE: a function has at most one limit at every point of its domain, isolated points included is false.
-
The sequential analogue is A sequence has at most one limit, proved by the same two-estimates-at-one-index argument. Neither statement uses any choice principle.
-
One-sided limits inherit this. By The left and right limits of at , as limits of the restrictions of to and a one-sided limit is the limit of a restriction of , so applying this lemma to that restriction gives uniqueness there too; nothing has to be reproved.
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
Statement
Let and let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ).
-
Locality. Let and , and suppose there is a real with for every satisfying . Then (The - limit of at a limit point of ).
-
Restriction. Let with a limit point of , let and suppose . Then is a limit point of as well, and , where is the restriction of .
So the limit at sees only the values of on an arbitrarily small punctured neighbourhood of , and it survives shrinking the domain, provided the smaller domain still accumulates at . Together with At a limit point of the domain a function has at most one limit this is what makes the phrase the limit at a local notion.
The converse of claim 2 is false in general: a restriction may have a limit where the function has none, as the one-sided limits of the sign function on the companion page show.
Facts & Assumptions
Given: A set and a limit point of ; for claim 1 functions , a real and a real with for every satisfying ; for claim 2 a subset having as a limit point, a function and a real with (The - limit of at a limit point of , Limit point, isolated point, adherent point, derived set, and dense subset of ).
The limit condition: means that for every real there is a real such that every in the domain of with satisfies (The - limit of at a limit point of ).
Limit point: is a limit point of a set 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 ).
Order arithmetic: of two positive reals the smaller is positive, the order being total; and gives (Ordered field).
Absolute value (Basic properties of the absolute value); and uniqueness of the limit at a limit point (At a limit point of the domain a function has at most one limit), which is what makes the phrase "the limit" in the statement denote.
Proof
For claim 1, assume and let be an arbitrary real.
For claim 2, and is a limit point of ; hence is a limit point of , since for every real a point with is also a point of with .
For claim 2, assume and let be an arbitrary real.
By [L1] fix a real such that every with satisfies , and put to be the smaller of and , so .
By [L1] fix a real such that every with satisfies .
Every with satisfies both and , so and ; as was arbitrary, .
Every with lies in and satisfies , so and therefore ; as was arbitrary, and is a limit point of , .
The hypothesis of claim 1 is symmetric in and , so interchanging their roles in steps 1.1, 2.1 and 3.1 gives the implication in the other direction, and claim 1 is proved; claim 2 is steps 1.2 and 3.2.
Remarks
-
What claim 1 is used for. It is the licence to modify a function outside a punctured neighbourhood of , or at itself, without changing the limit; the change at alone is already invisible to The - limit of at a limit point of , since the condition excludes that point.
-
What claim 2 is used for. It is the step that lets a statement proved on be transported to a smaller domain: the one-sided limits of The left and right limits of at , as limits of the restrictions of to and are exactly limits of restrictions, and the quotient case of Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero is proved on the smaller domain where the denominator does not vanish.
-
Both claims are choice free. Only the - definition is used; no sequence is constructed anywhere in the proof.
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.
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.
Heine criterion: iff for every sequence in converging to
Statement
Let , let , let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ) and let . The following are equivalent.
- (The - limit of at a limit point of ).
- For every sequence with and for every , and (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals), the sequence converges to .
The two directions do not cost the same. The implication from 1 to 2 is proved in ZF: the sequence is handed to the proof, and nothing is selected. The implication from 2 to 1, as proved below, invokes the axiom of countable choice (The Axiom of Countable Choice ()) exactly once, at step 3.2, to select one bad point from each of countably many nonempty sets. What this library does and does not claim about that cost is recorded in The sequence-to- direction of the Heine criterion uses countable choice for , and where this library records that cost; the same asymmetry appears, for the same reason, in A point lies in the closure of iff some sequence in converges to it, so a subset of is closed iff it is sequentially closed.
Because of this, the results on this page that can be proved directly from and — the algebra of limits, order preservation, the squeeze theorem, composition — are proved that way, and not through this criterion. What the criterion is for is the transfer of sequential results to functions, and above all the negative use recorded in A function has no limit at as soon as two sequences in tending to give different limits of the values, which needs only the choice-free direction.
Facts & Assumptions
Given: A set , a function , a limit point of and a real . Sequences are functions on , and contains (Sequences of reals: bounded, eventually, frequently, tails, subsequences, The natural numbers (von Neumann)), so the shrinking radii used below are and never .
The function limit: means that for every real there is a real such that every with satisfies (The - limit of at a limit point of ).
Sequential convergence: means that for every rational there is with for all (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences). Testing instead against every positive REAL defines 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), which is the passage sanctioned in the remarks of Sequences of reals: bounded, eventually, frequently, tails, subsequences.
Limit point: 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 ).
Reciprocal Archimedean property: for every real there is a natural with (For every in a complete ordered field there is a natural with , Every complete ordered field is Archimedean); the canonical naturals satisfy and are strictly increasing in (Canonical naturals are positive and strictly increasing); and gives (Inverses of positives are positive, and reciprocation reverses order).
Countable choice: for every family of nonempty sets there is a function with for every (The Axiom of Countable Choice ()).
Absolute value (Basic properties of the absolute value); and trichotomy, so the negation of is , and the negation of "for every there is such that P" is "there is such that for every , not P" (Ordered field).
Proof
Assume condition 1, let be a sequence with and for every and , and let be an arbitrary real.
Assume condition 1 FAILS. Negating the quantifiers of [L1], there is a real such that for every real some has and .
By [L1] fix a real such that every with satisfies ; and by [L2], being a positive real, fix with for every .
For put . Each is nonempty, since makes a positive real and step 1.2 applies to that radius.
For every we have and , so and hence . Since was an arbitrary real, ; condition 1 therefore implies condition 2.
By countable choice applied to the family , fix a function with for every .
That sequence has and for every , and it converges to : given a real , [L4] supplies a natural with , and every has , hence .
Yet does not converge to : every has , while a rational with ([L2]) would require some with for all .
So the failure of condition 1 produces a sequence witnessing the failure of condition 2; contrapositively, condition 2 implies condition 1, and with step 3.1 the two conditions are equivalent.
Remarks
-
Where the choice is spent, and where it is not. Step 3.2 is the only use of The Axiom of Countable Choice () in this proof, and it occurs only in the direction from condition 2 to condition 1. Steps 1.1, 2.1 and 3.1, which prove the other direction, use no choice principle. The sequence-to- direction of the Heine criterion uses countable choice for , and where this library records that cost says what may and may not be concluded from that.
-
The sets genuinely have no canonical element. They are cut out by an inequality involving , about which nothing is assumed, so there is no rule in this library that picks a point of uniformly in . That is exactly the situation The Axiom of Countable Choice () exists for, and it is the same situation as in A point lies in the closure of iff some sequence in converges to it, so a subset of is closed iff it is sequentially closed.
-
Why and not . Sequences here are functions on and contains (Sequences of reals: bounded, eventually, frequently, tails, subsequences), so the index occurs and would be undefined there. The same convention is used in A point lies in the closure of iff some sequence in converges to it, so a subset of is closed iff it is sequentially closed.
A function has no limit at as soon as two sequences in tending to give different limits of the values
Statement
Let , let and let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ). Then has no limit at — that is, no satisfies (The - limit of at a limit point of ) — as soon as either of the following occurs.
- There are sequences and with all terms in , both converging to , and reals with and (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).
- There is a sequence with all terms in , converging to , for which does not converge.
Only the choice-free half of the Heine criterion is used. The proof runs the implication from condition 1 to condition 2 of Heine criterion: iff for every sequence in converging to , which is a theorem of ZF; no sequence is constructed here, both being supplied by the hypothesis. So this corollary, the workhorse for showing that a limit fails to exist, costs no choice principle at all.
Facts & Assumptions
Given: A set , a function and a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of , The - limit of at a limit point of ).
Heine criterion, the direction from the - limit to sequences: if then for every sequence with all terms in converging to (Heine criterion: iff for every sequence in converging to ). That direction is proved without any choice principle.
A sequence of reals has at most one limit, so two limits of the same sequence are equal, and a sequence with a limit converges (A sequence has at most one limit, Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences).
Proof
Each of the two claims has the form "hypothesis has no limit at "; we prove the contrapositive of each, namely that if some satisfies then neither hypothesis can hold.
Assume there is with .
Let be an arbitrary sequence with all terms in converging to . By [L1], converges, with limit .
Under hypothesis 1 this applies to and to : and give by [L2], and likewise , so ; hypothesis 1, which asserts , therefore fails.
Under hypothesis 2 it applies to and gives that converges; hypothesis 2, which asserts that it does not, therefore fails.
So the existence of a limit of at excludes both hypotheses; contrapositively, either hypothesis excludes the existence of a limit of at .
Remarks
-
This is the standard way a limit is shown not to exist, and the reason is that the direct route would have to refute a statement beginning "there exists ": one would have to argue about every real at once. Two sequences reduce that to a single computation, as on the companion page for at and for the indicator of at every point.
-
The hypothesis "all terms in " is not decorative. A sequence allowed to take the value carries information about , which The - limit of at a limit point of deliberately ignores; the constant sequence would then refute every limit at once.
-
What the corollary does not say. It gives a sufficient condition for the limit not to exist, not a necessary one in any weaker form: the converse statement, that a limit exists as soon as all such image sequences converge to one value, is the other direction of Heine criterion: iff for every sequence in converging to and is exactly the direction that spends countable choice (The sequence-to- direction of the Heine criterion uses countable choice for , and where this library records that cost).
If has a finite limit at then is bounded on some punctured neighbourhood of
Statement
Let , let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ), let and suppose the limit of at exists, say (The - limit of at a limit point of ). Then there are a real and a real with
equivalently, the image is a bounded subset of (Lower bound, bounded below, bounded set, The -neighbourhood and the punctured -neighbourhood of a point of ). One may take .
Only local boundedness follows, never boundedness on . A function with a limit at may be unbounded on its domain, as FALSE: a function with a limit at is bounded on its whole domain records.
Facts & Assumptions
Given: A set , a limit point of , a function and a real with (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 (The - limit of at a limit point of ).
Absolute value: ; ; and for , is equivalent to (Basic properties of the absolute value).
Triangle inequality: (The triangle inequality).
Order arithmetic: (The multiplicative identity is positive); adding a constant preserves the order and adding inequalities is legitimate (Order is preserved by adding a constant and by adding inequalities); and implies . Order is preserved by adding a constant and by adding inequalities states these 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).
Bounded set: is bounded when it has both an upper and a lower bound (Lower bound, bounded below, bounded set); and (The -neighbourhood and the punctured -neighbourhood of a point of ).
Proof
Apply [L1] with the particular value , legitimate since : fix a real such that every with satisfies .
Put . Then , since and .
For every with we have , hence .
Therefore for every such , so is an upper bound and a lower bound of the image : that image is a bounded subset of .
Remarks
-
The radius depends on and and on nothing else here, since the proof runs the limit condition at the single value . Any other positive would do, with ; the value is chosen only because it is available in every ordered field (The multiplicative identity is positive).
-
Why this is needed. It is the hypothesis that makes the product case of Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero work: to estimate one needs a bound on near , and the limit of supplies one only locally. The companion fact for the denominator of a quotient — a lower bound on near — is If then on a punctured neighbourhood of ; in particular if then there.
-
The converse fails. A function bounded on a punctured neighbourhood of need not have a limit at : the oscillator on the companion page takes only values in and has no limit at .
If then on a punctured neighbourhood of ; in particular if then there
Statement
Let , let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ), let and suppose the limit of at exists with and (The - limit of at a limit point of ). Then there is a real such that every with satisfies
in particular for every such . Moreover:
- if then for every such ;
- if then for every such .
Consequently, writing
the point is a limit point of .
The bound , and not merely "", is what later proofs need. The quotient case of Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero estimates near and therefore needs a positive lower bound on there, and the last claim is what lets a limit be taken on the smaller domain at all.
Facts & Assumptions
Given: A set , a limit point of , a function 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 (The - limit of at a limit point of ).
Absolute value: ; if and only if ; for and for ; and for , is equivalent to (Basic properties of the absolute value).
Reverse triangle inequality: (The reverse triangle inequality).
Limit point: 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 ).
Order arithmetic in : trichotomy, so with and forces ; (The multiplicative identity is positive), hence and (Inverses of positives are positive, and reciprocation reverses order), so and for (Sign rules for products and monotonicity of multiplication); adding a constant to an inequality (Order is preserved by adding a constant and by adding inequalities); and of two positive reals the smaller is positive, the order being total (Ordered field).
Proof
Since we have while , so trichotomy gives , and with .
Apply [L1] with this : fix a real such that every with satisfies .
For every such the reverse triangle inequality gives , hence and so ; in particular and therefore .
If then , and for every such the estimate gives , that is .
If then , and for every such the estimate gives , that is .
Let be an arbitrary real and let be the smaller of and , so . Since is a limit point of there is with ; that satisfies , hence by step 3.1, so and . As was arbitrary, is a limit point of .
So on the function is bounded away from by and carries the sign of , and remains a limit point of the set where does not vanish.
Remarks
-
Why and not some other fraction. Any strictly between and gives a positive lower bound ; the choice makes the bound , which is the form used downstream and needs only that is invertible and positive (The multiplicative identity is positive, Inverses of positives are positive, and reciprocation reverses order).
-
The last claim is the one that is easy to forget. Restricting a quotient to the set where the denominator does not vanish is useless unless is still a limit point of that set, since The - limit of at a limit point of is stated only at a limit point. Step 4.1 is exactly that check, and it is what Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero cites when it forms .
-
Nothing here says anything about . As always the point itself is excluded by , so may be even when ; the function of FALSE: whenever both sides exist, read with the roles of and exchanged, is such an example.
Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero
Statement
Let , let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ), let and let . Suppose the limits of and of at exist, and write and (The - limit of at a limit point of ). Then:
- the limit of at exists, and
- the limit of at exists, and
- the limit of at exists, and
- if , then, writing , the point is a limit point of , the quotient is defined on by , the limit of at exists, and
Each equation asserts two things at once: that the limit on the left exists, and that it has the stated value. Both are proved. The symbols denote by At a limit point of the domain a function has at most one limit.
Everything below is proved directly from and . No sequence is constructed and no choice principle is used, so all four claims are theorems of ZF. Passing through Heine criterion: iff for every sequence in converging to instead would import the countable choice spent in that theorem's converse direction, for no gain; see The sequence-to- direction of the Heine criterion uses countable choice for , and where this library records that cost.
Why the quotient is stated on . The function is simply not defined where vanishes, and may well vanish at points of arbitrarily far from ; restricting to is therefore forced. That this restriction still has as a limit point, so that the limit there means anything at all, is the last claim of If then on a punctured neighbourhood of ; in particular if then there. The sequential analogue Algebra of limits: sums, scalar multiples, products and quotients needs the corresponding hypothesis in the form "the denominator sequence is nonzero at every index".
Facts & Assumptions
Given: A set , a limit point of , functions , a real , and reals with and ; for claim 4 also and (The - limit of at a limit point of , Limit point, isolated point, adherent point, derived set, and dense subset of ).
The limit condition: means that for every real there is a real such that every in the domain of with satisfies (The - limit of at a limit point of ).
Absolute value: ; if and only if ; ; and (Basic properties of the absolute value).
Triangle inequality: (The triangle inequality).
Order and field arithmetic in : adding two strict inequalities (Order is preserved by adding a constant and by adding inequalities); for , is equivalent to , and with gives (Sign rules for products and monotonicity of multiplication); positive elements have positive inverses and gives (Inverses of positives are positive, and reciprocation reverses order); (The multiplicative identity is positive), so and for ; inverses and the field identities (Field); trichotomy and totality, so of finitely many positive reals the smallest is positive (Ordered field).
Local boundedness: there are a real and a real with for every satisfying (If has a finite limit at then is bounded on some punctured neighbourhood of ).
Sign preservation: if there is a real with for every satisfying , and is a limit point of (If then on a punctured neighbourhood of ; in particular if then there).
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).
Neighbourhoods (The -neighbourhood and the punctured -neighbourhood of a point of ).
Proof
Sum. Let be an arbitrary real. By [L1] fix reals with for every satisfying and for every satisfying , and let be the smaller of the two, so . For with we get . As was arbitrary, the limit of at exists and equals : claim 1.
Scalar multiple. If then is the constant function and , so for every and every , any serving. If then ; given a real , [L1] supplies with on , and there . So the limit of at exists and equals : claim 2.
A working bound for near . By [L5] fix a real and a real with for every satisfying , and put , so and for all those .
The denominator near . Assume . By [L6] fix a real with for every satisfying ; every such has , hence lies in , and is a limit point of .
Product. Let be an arbitrary real. By [L1] fix reals with on and on , and let be the smallest of , which is positive. For with , . As was arbitrary, the limit of at exists and equals : claim 3.
Reciprocal. Assume and let be an arbitrary real. By [L1] fix a real with on , and let be the smaller of and . For with we have , hence and so ; therefore . As was arbitrary, the limit of at exists and equals .
The numerator on the smaller domain. Assume . Since and is a limit point of by step 1.4, [L7] gives that the limit of at exists and equals .
Quotient. Assume . On the domain , which has as a limit point, the two functions and have limits and at by steps 2.3 and 2.2, and their product is by the field identities; so claim 3, applied on the domain , gives that the limit of at exists and equals .
Claims 1 to 4 are proved, each directly from the - definition and none of them through a sequence.
Remarks
-
The product estimate in one line. The identity turns the problem into two products, one with a factor that is merely bounded near (that is , and If has a finite limit at then is bounded on some punctured neighbourhood of is what bounds it) and one with a constant factor. The two constants and are used in place of and only so that they are strictly positive and may be divided by; that is the sole reason for adding .
-
The reciprocal estimate in one line. The identity turns the problem into a numerator that is small and a denominator that must be kept away from ; the lower bound from If then on a punctured neighbourhood of ; in particular if then there does exactly that, and gives the working factor .
-
Nothing here extends to . The statement is about a finite limit point and finite values ; Limits at and , and infinite limits at a point introduces limits at and to infinity, but no algebra of such limits is proved in this library, and none may be assumed. The companion page's limit at is computed by a direct estimate for precisely that reason.
-
The sequential analogue is Algebra of limits: sums, scalar multiples, products and quotients. Neither implies the other for free: this theorem is about a function on a subset of and is proved from and ; that one is about sequences.
If on a punctured neighbourhood of then , non-strictly
Statement
Let , let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ), let and suppose both limits at exist (The - limit of at a limit point of ). Suppose further that there is a real with
Then
The conclusion is non-strict even when the hypothesis is strict. Replacing by on both sides gives a false statement, refuted by FALSE: near implies : strictness is destroyed in the limit, and no hypothesis short of a uniform gap restores it.
Only the values near matter, by 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 hypothesis is imposed on a punctured neighbourhood of and on nothing else, and it says nothing about and , which the definition ignores in any case.
Facts & Assumptions
Given: A set , a limit point of , functions , reals with and , and a real with for every satisfying (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 and (The - limit of at a limit point of ).
Limit point: 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 ).
Absolute value: for , is equivalent to (Basic properties of the absolute value).
Order arithmetic in : the order is total, so the negation of is ; trichotomy, so and cannot both hold; adding a constant to an inequality and adding two inequalities (Order is preserved by adding a constant and by adding inequalities); (The multiplicative identity is positive), so , (Inverses of positives are positive, and reciprocation reverses order) and for (Sign rules for products and monotonicity of multiplication), with ; and of finitely many positive reals the smallest is positive (Ordered field).
Proof
Suppose, for contradiction, that fails; the order being total, this means .
Then , so , and .
By [L1] fix reals such that every with has and every with has ; let be the smallest of , and , so .
Since is a limit point of , fix with .
That satisfies and , so gives and gives ; since , this yields .
But that same satisfies , so the hypothesis gives , which together with contradicts trichotomy.
The assumption that fails is therefore untenable, and .
Remarks
-
Both limits are assumed to exist. Nothing here proves existence: the statement compares two numbers that are given. The theorem that produces a limit from an order hypothesis is the squeeze theorem If near and and have the same limit at , then so does , whose conclusion is exactly the existence of the middle limit.
-
The special case says that a function which is non-negative near has a non-negative limit there. Its contrapositive is the form used in practice: a negative limit forces negative values near , which is a weak version of If then on a punctured neighbourhood of ; in particular if then there.
-
The sequential analogue is Limits preserve non-strict inequalities, and it too is non-strict for the same reason: the counterexample is a strict inequality between quantities whose difference tends to .
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.
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.
Composition of limits holds under either hypothesis: is defined at with value , or avoids on a punctured neighbourhood of
Statement
Let , let with , and let , so that the composite is defined. Let be a limit point of and a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ), and suppose the limits
both exist, with the stated values (The - limit of at a limit point of ). Suppose in addition that at least one of the following holds:
- (i) and ;
- (ii) there is a real with for every satisfying .
Then the limit of at exists, and
At least one extra hypothesis is necessary. With both omitted the statement is false, and FALSE: whenever and refutes it with a two-line witness in which (i) fails because and (ii) fails because is constantly equal to .
Why an extra hypothesis is needed at all. The inner limit controls only up to ; it does not prevent from equalling . But The - limit of at a limit point of says nothing about at the point , so the outer estimate is unavailable exactly at the values . Hypothesis (i) supplies the missing value directly; hypothesis (ii) excludes those values.
Facts & Assumptions
Given: Sets , functions with and , a limit point of , a limit point of , and reals with and ; and the assumption that (i) or (ii) of the statement holds (The - limit of at a limit point of , Limit point, isolated point, adherent point, derived set, and dense subset of ).
The limit condition: means that for every real there is a real such that every in the domain of with satisfies (The - limit of at a limit point of ).
Absolute value: , and if and only if (Basic properties of the absolute value).
Order arithmetic: of two positive reals the smaller is positive, the order being total; and trichotomy (Ordered field).
Limit point, and neighbourhoods (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ).
Proof
Let be an arbitrary real. By [L1] applied to at , fix a real such that every with satisfies ; then by [L1] applied to at , with in the role of the tolerance, fix a real such that every with satisfies .
Case (i): assume and , and put . Let with and set , an element of since ; then . If then ; and if then , so . In both events .
Case (ii): assume there is a real with for every satisfying , and let be the smaller of and , so . Let with and set ; then , so , and , so and .
By hypothesis at least one of (i) and (ii) holds, so in either case a real has been produced with for every satisfying ; since was arbitrary and is a limit point of , the limit of at exists and equals .
Remarks
-
The hypothesis that is a limit point of is what makes meaningful at all (The - limit of at a limit point of ); it is not an extra assumption of convenience. Note that it does not follow from : a constant has that limit while may be a set for which is isolated.
-
Hypothesis (i) is the continuity hypothesis in disguise. Saying and is exactly saying that is continuous at in the sense the next page of this track will define; that is the form in which this theorem is usually quoted, and it is why textbook statements of "the limit of a composition" almost always assume continuity of the outer function.
-
Hypothesis (ii) is the one that survives without continuity, and it is the hypothesis under which substitutions such as are legitimate: there the inner function omits the critical value on a punctured neighbourhood for a structural reason, not by assumption on .
-
The two hypotheses are genuinely different, neither implying the other. The companion page exhibits a pair satisfying neither, and the same pair with the inner function replaced by the identity, which satisfies (ii) but not (i).
Integer part: for every real there is exactly one integer with
Statement
Identify with its canonical copy inside , along the embeddings (The naturals embed in the integers, The integers embed in the rationals, The rationals embed densely in the reals, The integers as equivalence classes of pairs of naturals). Then for every real there is exactly one integer with
It is written and called the integer part, or floor, of .
Two independent ingredients are needed and neither may be dropped. Existence is the Archimedean property (Every complete ordered field is Archimedean) together with the well-ordering of (The well-ordering principle): the first says that is caught between two integers at all, the second picks the least integer above . Uniqueness is the discreteness of : no integer lies strictly between and .
This lemma is stated once here and reused. It is what turns "the nearest integer to " from a picture into an object, and the companion page's oscillator is computed from it in one line.
Facts & Assumptions
Given: A real . Naturals, integers and rationals are identified with their canonical copies in along .
The embeddings are injective and preserve , , addition, multiplication and order (The naturals embed in the integers, The integers embed in the rationals, The rationals embed densely in the reals, The integers as equivalence classes of pairs of naturals); is a totally ordered commutative ring (The integers form a totally ordered ring, The integers form a commutative ring); every integer is the image of a unique natural, that map being injective and order preserving (The naturals embed in the integers); and a natural satisfies (Discreteness: is the immediate successor, The natural numbers (von Neumann)).
The image of a natural under the composite is the canonical natural of Canonical naturals are positive and strictly increasing. Indeed that composite preserves and addition by [L1], while is defined by and , so the two agree at and satisfy the same recursion; induction on (The principle of mathematical induction) gives the identification.
Archimedean property: for every real there is a natural with (Every complete ordered field is Archimedean, Complete ordered field (least-upper-bound property)).
Well-ordering principle: every nonempty subset of has a least element (The well-ordering principle).
Order arithmetic in : the order is total, so the negation of is ; trichotomy, so and cannot both hold; translation invariance (Order is preserved by adding a constant and by adding inequalities); and (Basic properties of the absolute value); and transitivity (Ordered field, Complete ordered field (least-upper-bound property)).
Proof
Apply [L3] to the real : fix a natural with . Since and , this gives .
Put , where is formed in and read in through [L1]. It is a subset of , and it is nonempty: the natural satisfies by step 1.1, so .
By the well-ordering principle [L4] let be the least element of .
The index is not : for the defining condition reads , which trichotomy excludes since by step 1.1. Hence , so by [L1], and is again a natural number.
Set , an integer. Since and is the least element of , the natural does not lie in , that is, fails; the order being total, .
On the other hand gives . So , and existence is proved.
Uniqueness: suppose an integer also satisfies and . The order of being total, one of and holds, and the two cases are the same with the roles of and exchanged; so assume . Then is an integer , hence by [L1] the image of a natural , so and , that is . But then , which trichotomy forbids. Hence .
Therefore exactly one integer satisfies , and we write .
Remarks
-
What the two halves of the proof really use. Step 1.1 is the only use of the Archimedean property, and it is indispensable: in a non-Archimedean ordered field (Not every ordered field is Archimedean) an element larger than every canonical natural has no integer part at all, since the set of step 2.1 would be empty. Step 3.1 is the only use of the well-ordering principle, and it is what makes the construction canonical: no choice is made anywhere, and is a function of .
-
Immediate consequences, used later. From one reads off and ; and exactly when is an integer, since an integer satisfies and uniqueness does the rest. The translation identity for an integer follows the same way: adding to gives , and uniqueness identifies as the integer part of .
-
The ceiling is not defined here and is not needed on this page; it would be the least integer , obtained from the same set without the shift by one.
The sequence-to- direction of the Heine criterion uses countable choice for , and where this library records that cost
What this page spends, and where
Heine criterion: iff for every sequence in converging to is an equivalence, and its two directions do not cost the same.
-
From the - limit to sequences — if then for every sequence in tending to — is proved in ZF. The sequence is handed to the proof; nothing is selected. This is steps 1.1, 2.1 and 3.1 of that theorem.
-
From sequences to the - limit is proved there using the Axiom of Countable Choice (The Axiom of Countable Choice ()), invoked exactly once, at step 3.2. The proof assumes the limit fails, obtains for each a nonempty set , and needs a single point from each of those countably many sets at once.
Why no canonical selection is available. The sets are cut out by an inequality involving , about which the theorem assumes nothing. There is therefore no rule in this library that names an element of uniformly in : they are subsets of , which carries no well-ordering that ZF provides, and the sets need not be intervals, need not be closed, and need not meet . That is precisely the situation The Axiom of Countable Choice () exists for.
The same cost, recorded twice
The identical pattern occurs in the prerequisite page: in A point lies in the closure of iff some sequence in converges to it, so a subset of is closed iff it is sequentially closed the right-to-left direction is choice free, while producing a sequence in converging to a point of requires selecting one point of from each of the sets , and that item invokes explicitly for it. Both items name the step where the axiom is used, so a reader working in ZF alone can see exactly which half of each equivalence survives.
What this library claims, and what it does not
-
Claimed: the direction from - to sequences is a theorem of ZF; the converse as proved here uses ; and the use is isolated to one step, so nothing else on this page inherits it.
-
Not claimed: that the converse requires . This library proves no independence result and contains neither forcing nor permutation models, so it is in no position to assert that some cleverer ZF proof does not exist. The systematic study of which such criteria need which fragment of choice is a subject in its own right; Herrlich's Axiom of Choice is the standard reference, and it is cited here as literature, not used.
-
A warning against a tempting slogan. It is not the case that sequential criteria in analysis always need choice. Sierpiński proved, in ZF, that a function which is sequentially continuous at every point is continuous. The everywhere-statement and the pointwise-statement behave differently, and the cost recorded above is a statement about the pointwise criterion as proved here, nothing more.
The consequence for how this page is organised
Because the criterion carries a choice cost on one side, this page does not route its main results through it. The algebra of limits (Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero), order preservation (If on a punctured neighbourhood of then , non-strictly), the squeeze theorem (If near and and have the same limit at , then so does ) and composition (Composition of limits holds under either hypothesis: is defined at with value , or avoids on a punctured neighbourhood of ) are all proved directly from and , and are therefore theorems of ZF. The sequential machinery is used only where it earns its place: in the criterion itself, and in A function has no limit at as soon as two sequences in tending to give different limits of the values, which needs only the choice-free direction and is the tool by which the companion page shows that various limits fail to exist.
That organisation is a deliberate choice of proofs, not a mathematical necessity: each of those four results could be deduced from the criterion, at the price of importing into statements that do not need it.
5 · Examples, counterexamples and false statements
FALSE: whenever both sides exist
Statement
False claim: if , if , if is a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ) and if the limit of at exists (The - limit of at a limit point of ), then
Both sides of the asserted equation are defined under the stated hypotheses: the left because the limit is assumed to exist and is single valued (At a limit point of the domain a function has at most one limit), the right because . The claim is that they always agree, and that is false.
Why it is tempting. The condition is imposed on points arbitrarily close to , and it feels as though were the limiting case of that. It is not: The - limit of at a limit point of quantifies over , and the strict inequality on the left removes from the quantifier entirely. Changing the value of at the single point therefore changes nothing on the left-hand side and everything on the right.
What is true. The equation above is not a theorem but a condition, and it is the condition the next page of this track takes as the definition of continuity at . This library states it as a hypothesis and never as a consequence; hypothesis (i) of Composition of limits holds under either hypothesis: is defined at with value , or avoids on a punctured neighbourhood of is exactly this condition for the outer function.
Facts & Assumptions
Given: The set , the point , and the function defined by for and .
The limit condition: means that for every real there is a real such that every in the domain of with satisfies (The - limit of at a limit point of ).
Limit point: is a limit point of when every punctured neighbourhood meets ; and punctured neighbourhoods in are never empty (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ).
Absolute value: , and (Basic properties of the absolute value).
Order in : trichotomy, so every real either equals or does not, and never both; and , so (The multiplicative identity is positive, Ordered field).
Refutation
The point lies in and is a limit point of : for every real the punctured neighbourhood is nonempty and is contained in , so it meets .
is a well-defined function on , since by trichotomy every real either equals or does not, exclusively; and the reals and are distinct.
The limit of at exists and equals : given an arbitrary real , take ; every with has , hence , hence and .
Yet , and . So at the point of the domain, which is a limit point of the domain, the limit exists and differs from the value: the claim is false.
Remarks
-
The witness is the smallest possible one. It differs from a constant function at exactly one point, and the limit cannot see that point. Any function agreeing with a constant off and taking a different value at would serve equally well; the companion page works this witness out in full, computes its one-sided limits, and shows that redefining the single value repairs the equality.
-
Where the false claim does hold. Under the extra hypothesis that — which is what continuity at will mean — it holds trivially, and that is the only sense in which it is ever true. It is emphatically not a consequence of the limit existing.
-
The consequence for composition. Because is invisible to the limit, substituting an inner function that takes the value is not licensed by the limits alone; that is the content of FALSE: whenever and , whose witness is built from this one.
FALSE: whenever and
Statement
False claim: let , let with and , let be a limit point of and a limit point of . If
then the limit of at exists and (The - limit of at a limit point of ).
This is the statement of Composition of limits holds under either hypothesis: is defined at with value , or avoids on a punctured neighbourhood of with both of its extra hypotheses removed, and it is false. It is refuted below by a pair in which is constant and has a removable defect at the value of that constant.
Where the naive argument breaks. The inner limit gives for near ; the outer limit gives for with . To combine them at one needs , and nothing in the hypotheses supplies that. Where , the only information available about is its value , and The - limit of at a limit point of says nothing whatever about that value (FALSE: whenever both sides exist). The two hypotheses of Composition of limits holds under either hypothesis: is defined at with value , or avoids on a punctured neighbourhood of are exactly the two ways of closing that gap.
Facts & Assumptions
Given: The sets and ; the point ; the function of FALSE: whenever both sides exist, namely for and ; and the constant function , for every .
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 .
Every real is a limit point of , punctured neighbourhoods being never empty (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ).
Absolute value: (Basic properties of the absolute value).
Order in : trichotomy, and , so (The multiplicative identity is positive, Ordered field).
The function above satisfies and has limit at : for every real the radius works, since forces and then ; this is the computation carried out in FALSE: whenever both sides exist.
Composition of limits and its two extra hypotheses (i) and (ii) (Composition of limits holds under either hypothesis: is defined at with value , or avoids on a punctured neighbourhood of ).
Refutation
The point is a limit point of , and , so is a function on .
By [L5], ; so the outer hypothesis holds with and .
The reals and are distinct.
The inner hypothesis holds with : for the constant function and any real , every works, since for every . So .
But is the constant function : for every , and hence . Therefore, by the same computation as in step 2.1, the limit of at exists and equals .
Both extra hypotheses of Composition of limits holds under either hypothesis: is defined at with value , or avoids on a punctured neighbourhood of fail for this pair: hypothesis (i) fails because lies in while ; and hypothesis (ii) fails because for every , so no punctured neighbourhood of avoids the value .
So and , while : the claim is false, and step 3.2 identifies exactly which hypotheses of the true theorem are missing.
Remarks
-
The failure is not an artefact of the constant inner function. What matters is that takes the value on every punctured neighbourhood of ; a non-constant that hits along a sequence tending to would fail in the same way. Conversely, replacing by the identity — which avoids the value off the point itself — restores the conclusion, and the companion page carries out that comparison.
-
Textbook statements almost always assume continuity of the outer function, which is hypothesis (i) of Composition of limits holds under either hypothesis: is defined at with value , or avoids on a punctured neighbourhood of written out. The version with hypothesis (ii) is the one that licenses substitutions such as , where the inner function omits the critical value for a structural reason.
-
The same witness refutes nothing else on this page. In particular it does not bear on Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero: sums, products and quotients are formed pointwise from the values of and at the same argument, and no composition is involved.
FALSE: a function has at most one limit at every point of its domain, isolated points included
Statement
False claim: for every , every and every , at most one real satisfies
Read the claim carefully: it is about the raw formula , extended to an arbitrary point of the domain. It is not a claim about The - limit of at a limit point of . That definition imposes only when is a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ), and there at most one does satisfy it — that is exactly At a limit point of the domain a function has at most one limit, which is true and proved. The false claim is what one gets by deleting the limit-point requirement.
At an isolated point of the symbol is undefined in this library, and the refutation below is the reason. If is not a limit point of then some punctured neighbourhood of misses entirely (Limit point, isolated point, adherent point, derived set, and dense subset of ); the implication inside then has no instances at all for that , so it holds vacuously, and it holds for every real at once. A formula satisfied by every real determines nothing, so no notation is introduced for it.
Facts & Assumptions
Given: The set (Intervals of : the nine order-convex forms, nondegeneracy, and length), the constant function with for every , and the point .
The - formula above, and the fact that The - limit of at a limit point of imposes it only at a limit point of the domain.
Limit point and isolated point: is a limit point of when for every real , and is an isolated point of when for some real ; for these are exact opposites (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ).
Neighbourhoods: and (The -neighbourhood and the punctured -neighbourhood of a point of ).
Absolute value and order: ; exactly when ; for ; the order is total and trichotomy holds; and , so (Basic properties of the absolute value, The multiplicative identity is positive, Ordered field).
Refutation
The point lies in , and : an element of is either , which satisfies , or an element of , which satisfies and so is not in . Hence is an isolated point of and not a limit point of .
The reals and are distinct.
Take . No satisfies : such an would lie in , which is contained in and excludes , hence is empty. So for every real and every real the choice makes the implication in vacuously true, and every real satisfies at .
In particular and both satisfy at , and they are distinct: more than one real satisfies the formula, so the claim is false.
Remarks
-
This is the precise reason The - limit of at a limit point of carries the limit-point hypothesis. The hypothesis is not a convenience: it is what makes the quantified set nonempty for every , and hence what makes capable of pinning down. With it, At a limit point of the domain a function has at most one limit proves uniqueness; without it, uniqueness is simply false, as above.
-
The true statement in the neighbourhood of the false one. For a limit point of : at most one satisfies — At a limit point of the domain a function has at most one limit. For an isolated point of : every satisfies , by the argument of step 2.1, which uses nothing about . So the dichotomy is total, and there is no intermediate case, because for being isolated and being a limit point are exact opposites (Limit point, isolated point, adherent point, derived set, and dense subset of ).
-
Some texts do define the limit at an isolated point, declaring it to be by fiat, so that "limit" and "continuity" coincide on such points. That is a convention, not a theorem, and this library declines it: a convention that assigns a value to an expression which the definition leaves underdetermined would have to be carried, and checked, in every later statement about limits. The companion page's counterexample exhibits the underdetermination concretely.
FALSE: near implies
Statement
False claim: let , let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ), let have limits at (The - limit of at a limit point of ), and suppose there is a real with
Then .
What is true is the non-strict version, If on a punctured neighbourhood of then , non-strictly: the hypothesis near gives , and that conclusion cannot be improved even when the hypothesis is strengthened to a strict inequality at every point.
Why the strengthening fails. Strictness at each point is not a uniform statement: it says for every near , with no lower bound on that positive quantity. The limit only sees the limit of , and a function that is positive everywhere may have limit . What does survive is the uniform version: if near for a fixed real , then , by applying If on a punctured neighbourhood of then , non-strictly to and .
Facts & Assumptions
Given: The set , the point , the constant function with for every , and the function with .
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 .
Every real is a limit point of , punctured neighbourhoods being never empty (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ).
Absolute value: ; exactly when ; and for , so (Basic properties of the absolute value).
Order in : trichotomy, so together with gives , and is impossible (Ordered field).
Refutation
The point is a limit point of .
The strict hypothesis holds with : every with has , hence , that is .
Both limits exist and are equal to . For : for every and every real , any serving. For : given a real take ; every with satisfies .
So throughout a punctured neighbourhood of while ; the asserted strict inequality is impossible by trichotomy, so the claim is false.
Remarks
-
The non-strict conclusion is sharp, and this witness shows it: the hypothesis is as strong as a pointwise strict inequality can be, and the conclusion still degenerates to equality.
-
The same phenomenon for sequences is the reason Limits preserve non-strict inequalities is stated non-strictly; the witness there is a positive null sequence compared with the constant , which is the sequential shadow of the pair above.
-
A common misuse. From near one may conclude and nothing more; in particular one may not conclude that from near . To get a strict conclusion one needs either a uniform gap, as noted above, or a separate argument such as If then on a punctured neighbourhood of ; in particular if then there, which works in the opposite direction: from a nonzero limit to a bound on the values.
FALSE: a function with a limit at is bounded on its whole domain
Statement
False claim: let , let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ) and let have a limit at (The - limit of at a limit point of ). Then is bounded on , that is, the image is a bounded subset of (Lower bound, bounded below, bounded set).
What is true is the local statement, If has a finite limit at then is bounded on some punctured neighbourhood of : there is a radius such that is bounded on . The radius is produced by the limit condition at the single tolerance , and it carries no information whatever about the values of far from , which the limit condition never constrains.
The witness below is on at the point : the limit there is , and is bounded near , while on the whole domain takes values above every real.
Facts & Assumptions
Given: The set (Intervals of : the nine order-convex forms, nondegeneracy, and length), the point , and the function with .
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 and neighbourhoods (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ).
Absolute value: ; for ; ; ; and for , is equivalent to (Basic properties of the absolute value).
Inverses and order: gives , and gives (Inverses of positives are positive, and reciprocation reverses order); for , inverses being unique (Field); and for , is equivalent to (Sign rules for products and monotonicity of multiplication).
Order arithmetic: , hence and with (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities); of two positive reals the smaller is positive, the order being total (Ordered field).
Archimedean property: for every real there is a natural with , and the canonical naturals satisfy (Every complete ordered field is Archimedean, Canonical naturals are positive and strictly increasing, Complete ordered field (least-upper-bound property)).
Bounded set: is bounded when it has an upper bound and a lower bound; a set with no upper bound is not bounded (Lower bound, bounded below, bounded set).
Refutation
The point lies in and is a limit point of : given a real , let be the smaller of and , so ; then lies in and satisfies .
is well defined on : every has , hence and exists, with .
The limit of at exists and equals . Let be an arbitrary real and let be the smaller of and , so . For with we get , hence by [L4]; and .
The image has no upper bound. Let be an arbitrary real; by [L6] fix a natural with , and note . Then satisfies , so , and . So no real bounds above, and is not bounded.
So has a limit at the limit point of its domain and is unbounded on that domain: the claim is false, while If has a finite limit at then is bounded on some punctured neighbourhood of remains true and gives boundedness on , where indeed by step 2.1.
Remarks
-
The limit hypothesis is entirely local and the conclusion asked for is global, so no argument could bridge them. The witness makes that concrete by putting the unbounded behaviour at the other end of the domain, arbitrarily far from in the only sense available here.
-
The sequential analogue is true, and that contrast is worth noting: a convergent sequence is bounded (Every convergent sequence is bounded), because a sequence has only finitely many terms outside any tail, and finitely many reals are bounded. A function has no such structure: the part of outside a punctured neighbourhood of can be infinite and can carry arbitrary values.
-
A bounded version does hold with an extra hypothesis: if is itself contained in a punctured neighbourhood of on which the limit estimate applies, then local and global boundedness coincide. That is a hypothesis on the domain, not a theorem about limits.
Sources
Standard references
Recommended treatments; not extraction sources.
- J. Lebl, Basic Analysis I, §3.1: Limits of functions
- Limit of a function (Wikipedia)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 4 (Def. 4.1)
- T. Tao, Analysis I, 3rd ed., §9.3
- J. Lebl, Basic Analysis I, §3.1
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 4
- One-sided limit (Wikipedia)
- J. Lebl, Basic Analysis I, §3.5
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 4 (Thm 4.2)
- Axiom of countable choice (Wikipedia)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 4 (Cor. to Thm 4.2)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 4 (Thm 4.4)
- Squeeze theorem (Wikipedia)
- Floor and ceiling functions (Wikipedia)
- Archimedean property (Wikipedia)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1
- T. Tao, Analysis I, 3rd ed., §5.4
- H. Herrlich, Axiom of Choice, Lecture Notes in Mathematics 1876, Springer 2006
- Classification of discontinuities (Wikipedia)
- Isolated point (Wikipedia)