Alphabeta Math
Session-authored (Fable 5 assisted)
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.

17 results · all verified · 14 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Limits of Real Functions

1 · Prerequisites

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 R\mathbb{R} (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}) and on the theory of sequences, and it is the last page before continuity.

The definition, and the three decisions inside it. The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA says that limxcf(x)=L\lim_{x \to c} f(x) = L when for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 with f(x)L<ε|f(x) - L| < \varepsilon for every xx in the domain satisfying 0<xc<δ0 < |x - c| < \delta. Three features are load bearing rather than decorative, and two of the three have a false statement on this page attached to them.

Locality. The limit at cc depends only on the restriction of ff to a punctured neighbourhood of cc, and passes to any subset of the domain having cc as a limit point proves the two statements that make the limit a local object: changing ff outside a punctured neighbourhood of cc changes nothing, and a limit survives restricting the domain to any subset that still has cc 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 ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty) defines limxc±f(x)\lim_{x \to c^{\pm}} f(x) as the limit of the restriction of ff to the points of the domain on one side of cc, so uniqueness and locality are inherited rather than reproved. Limits at ++\infty and -\infty, and infinite limits at a point defines limits at ±\pm\infty, where the role of the limit-point hypothesis is played by unboundedness of the domain, and infinite limits at a point. The symbols ±\pm\infty remain abbreviations and never real numbers: the library does not write limxcf(x)=+\lim_{x \to c} f(x) = +\infty, for the reason Divergence to ++\infty and to -\infty already gave for sequences. Uniqueness of the limit at ±\pm\infty is proved inside that definition.

Choice hygiene, and why it shapes the page. Heine criterion: limxcf(x)=L\lim_{x \to c} f(x) = L iff f(xk)Lf(x_k) \to L for every sequence in A{c}A \setminus \{c\} converging to cc — the Heine criterion — says that limxcf(x)=L\lim_{x \to c} f(x) = L if and only if f(xk)Lf(x_k) \to L for every sequence in the domain avoiding cc and converging to cc. Its two directions do not cost the same. The direction from ε\varepsilon-δ\delta to sequences is a theorem of ZF. The converse, as proved here, invokes the axiom of countable choice (The Axiom of Countable Choice (ACω\mathrm{AC}_\omega)) 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 ARA \subseteq \mathbb{R} iff some sequence in AA converges to it, so a subset of R\mathbb{R} is closed iff it is sequentially closed on the prerequisite page. The sequence-to-ε\varepsilon direction of the Heine criterion uses countable choice for R\mathbb{R}, 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 ε\varepsilon and δ\delta 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 cc as soon as two sequences in A{c}A \setminus \{c\} tending to cc 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 cc 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 ff has a finite limit at cc then ff is bounded on some punctured neighbourhood of cc shows that a function with a limit at cc is bounded on some punctured neighbourhood of cc — and only there, which is FALSE: a function with a limit at cc is bounded on its whole domain. If limxcf(x)=L0\lim_{x \to c} f(x) = L \ne 0 then f>L/2|f| > |L|/2 on a punctured neighbourhood of cc; in particular if L>0L > 0 then f>L/2>0f > L/2 > 0 there shows that a nonzero limit LL forces f>L/2|f| > |L|/2 on a punctured neighbourhood, with the sign of LL, and that cc remains a limit point of the set where ff 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 fgf \le g on a punctured neighbourhood of cc then limflimg\lim f \le \lim g, non-strictly proves that fgf \le g near cc gives limflimg\lim f \le \lim g; the conclusion cannot be sharpened to a strict inequality even from a strict hypothesis, which is FALSE: f<gf < g near cc implies limf<limg\lim f < \lim g. If fghf \le g \le h near cc and ff and hh have the same limit at cc, then so does gg is the one result here that produces a limit rather than computing one: no hypothesis is placed on the squeezed function at all. If cc 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: ff is defined at LL with value MM, or gg avoids LL on a punctured neighbourhood of cc is false as usually first stated. The inner limit controls g(x)L|g(x) - L| but does not prevent g(x)g(x) from equalling LL, and at those arguments the outer limit says nothing, since it never sees f(L)f(L). Two hypotheses each close the gap, and either suffices: (i) LL lies in the outer domain with f(L)=Mf(L) = M, which is continuity of ff at LL written out; or (ii) gg avoids the value LL on a punctured neighbourhood of cc, which is what makes substitutions such as y=1/xy = 1/x legitimate. With both dropped the statement is refuted by FALSE: limxcf(g(x))=M\lim_{x \to c} f(g(x)) = M whenever limxcg=L\lim_{x \to c} g = L and limyLf=M\lim_{y \to L} f = M, whose witness fails (i) and (ii) at once.

One reusable lemma, deliberately placed here. Integer part: for every real xx there is exactly one integer mm with mx<m+1m \le x < m + 1 proves that every real xx has exactly one integer mm with mx<m+1m \le x < m+1. Existence is the Archimedean property together with the well-ordering of N\mathbb{N}; uniqueness is the discreteness of Z\mathbb{Z}. 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 ψ(x)=infnZxn\psi(x) = \inf_{n \in \mathbb{Z}} |x - n| in one line.

The companion page carries the witnesses: polynomials and rational functions, the oscillator ψ\psi and the two examples built on it, the sign function, a limit at ++\infty computed by a direct estimate, the indicator of Q\mathbb{Q}, 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

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA

Definition

Throughout, R\mathbb{R} is the complete ordered field (Complete ordered field (least-upper-bound property)) with its order and absolute value (Order on the reals).

Let ARA \subseteq \mathbb{R}, let f:ARf : A \to \mathbb{R}, let cRc \in \mathbb{R} be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}), and let LRL \in \mathbb{R}. We say that f(x)f(x) tends to LL as xx tends to cc, and write

limxcf(x)=L,\lim_{x \to c} f(x) = L ,

when

(ε>0) (δ>0) (xA) [ 0<xc<δ  f(x)L<ε ],(\forall \varepsilon > 0)\ (\exists \delta > 0)\ (\forall x \in A)\ \bigl[\ 0 < |x - c| < \delta \ \Longrightarrow\ |f(x) - L| < \varepsilon\ \bigr],

where ε\varepsilon and δ\delta range over the positive reals.

In the language of neighbourhoods (The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}) the condition reads: for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 with

f(ANδ(c))    Nε(L),f\bigl(A \cap N^{*}_{\delta}(c)\bigr) \;\subseteq\; N_{\varepsilon}(L),

Nδ(c)={y:0<yc<δ}N^{*}_{\delta}(c) = \{\, y : 0 < |y - c| < \delta \,\} being the punctured δ\delta-neighbourhood of cc and Nε(L)=(Lε, L+ε)N_{\varepsilon}(L) = (L - \varepsilon,\ L + \varepsilon) the open interval of Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length. The two forms agree because f(x)L<ε|f(x) - L| < \varepsilon says exactly f(x)Nε(L)f(x) \in N_\varepsilon(L), and 0<xc<δ0 < |x - c| < \delta says exactly xNδ(c)x \in N^{*}_\delta(c).

Three features of this definition are load bearing, not decoration.

  1. cc is required to be a limit point of AA. By Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R} that says every punctured neighbourhood of cc meets AA, so for every δ>0\delta > 0 the set ANδ(c)A \cap N^{*}_\delta(c) over which the implication quantifies is nonempty. Drop the requirement and the implication can be satisfied vacuously by every real LL 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 AA that is not a limit point of AA — an isolated point — the symbol limxcf(x)\lim_{x \to c} f(x) is therefore not defined in this library.

  2. cAc \in A is not required. A limit point of AA need not belong to AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}), and the definition never evaluates ff at cc. This is what allows a limit to be taken at a point where the function is not defined at all, as at 00 for xxψ(1/x)x \mapsto x\,\psi(1/x).

  3. The value f(c)f(c), when it exists, is irrelevant. The hypothesis 0<xc0 < |x - c| excludes x=cx = c from the quantifier, so changing ff at the single point cc changes nothing. Equality of the limit with the value is an extra condition, not a consequence: FALSE: limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) whenever both sides exist.

The notation presumes uniqueness. Writing limxcf(x)=L\lim_{x \to c} f(x) = L 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 LL 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 supS\sup S (Conventions: sup\sup \emptyset, unbounded sets, and the extended reals) and limkxk\lim_k x_k (A sequence has at most one limit), the symbol is written only for a function already known to have a limit at cc.

Real and rational ε\varepsilon define the same relation. Above, ε\varepsilon and δ\delta 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 ε\varepsilon-condition verified for all positive rationals is verified for an arbitrary positive real η\eta by running it at a rational ε\varepsilon with 0<ε<η0 < \varepsilon < \eta, and a δ\delta 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 ε\varepsilon is rational, in Heine criterion: limxcf(x)=L\lim_{x \to c} f(x) = L iff f(xk)Lf(x_k) \to L for every sequence in A{c}A \setminus \{c\} converging to cc.

Remarks

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

At a limit point of the domain a function has at most one limit

Statement

Let ARA \subseteq \mathbb{R}, let f:ARf : A \to \mathbb{R}, let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}) and let L,LRL, L' \in \mathbb{R}. If

limxcf(x)=Landlimxcf(x)=L\lim_{x \to c} f(x) = L \qquad \text{and} \qquad \lim_{x \to c} f(x) = L'

(The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA), then L=LL = L'.

A function therefore has at most one limit at a limit point of its domain, which is what licenses the notation limxcf(x)\lim_{x \to c} f(x) for a single real number. This lemma is recorded in the justified_by field of The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA for exactly that reason.

The hypothesis that cc is a limit point is not removable. At an isolated point of the domain the same ε\varepsilon-δ\delta 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 ARA \subseteq \mathbb{R}, a function f:ARf : A \to \mathbb{R}, a limit point cc of AA, and reals L,LL, L' with limxcf(x)=L\lim_{x \to c} f(x) = L and limxcf(x)=L\lim_{x \to c} f(x) = L' (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA, Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}).

[L1]

The limit condition: for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xAx \in A with 0<xc<δ0 < |x - c| < \delta satisfies f(x)L<ε|f(x) - L| < \varepsilon, and likewise with LL' in place of LL (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

[L2]

Limit point: for every real δ>0\delta > 0 there is xAx \in A with 0<xc<δ0 < |x - c| < \delta (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L3]

Triangle inequality: u+vu+v|u + v| \le |u| + |v| in R\mathbb{R} (The triangle inequality).

[L4]

Absolute value: u0|u| \ge 0; u=0|u| = 0 if and only if u=0u = 0; and u=u|-u| = |u| (Basic properties of the absolute value).

[L5]

Order arithmetic in R\mathbb{R}: trichotomy, so u0u \ne 0 together with u0|u| \ge 0 and u0|u| \ne 0 forces u>0|u| > 0, and t<tt < t is impossible; adding two strict inequalities (Order is preserved by adding a constant and by adding inequalities); 0<10 < 1 (The multiplicative identity is positive), hence 2:=1+1>02 := 1 + 1 > 0 and 21>02^{-1} > 0 (Inverses of positives are positive, and reciprocation reverses order), so η/2>0\eta/2 > 0 and (η/2)2=η(\eta/2) \cdot 2 = \eta whenever η>0\eta > 0 (Sign rules for products and monotonicity of multiplication, Ordered field); and of two positive reals the smaller is positive, the order being total.

Proof

technique · contradiction
1.1

Suppose, for contradiction, that LLL \ne L'.

assume-contra
2.1

Then LL0L - L' \ne 0, so LL0|L - L'| \ne 0 while LL0|L - L'| \ge 0, and trichotomy gives LL>0|L - L'| > 0; hence ε:=LL/2>0\varepsilon := |L - L'|/2 > 0 and 2ε=LL2\varepsilon = |L - L'|.

step 1.1L4L5
3.1

Applying [L1] twice with this ε\varepsilon, fix reals δ1>0\delta_1 > 0 and δ2>0\delta_2 > 0 such that every xAx \in A with 0<xc<δ10 < |x - c| < \delta_1 has f(x)L<ε|f(x) - L| < \varepsilon and every xAx \in A with 0<xc<δ20 < |x - c| < \delta_2 has f(x)L<ε|f(x) - L'| < \varepsilon; put δ\delta to be the smaller of δ1\delta_1 and δ2\delta_2, so δ>0\delta > 0.

step 2.1L1L5choose
4.1

Since cc is a limit point of AA, fix xAx \in A with 0<xc<δ0 < |x - c| < \delta.

step 3.1L2choose
5.1

That xx satisfies 0<xc<δ10 < |x - c| < \delta_1 and 0<xc<δ20 < |x - c| < \delta_2, hence both f(x)L<ε|f(x) - L| < \varepsilon and f(x)L<ε|f(x) - L'| < \varepsilon.

step 3.1step 4.1L1
6.1

Therefore LL=(Lf(x))+(f(x)L)Lf(x)+f(x)L=f(x)L+f(x)L<ε+ε=2ε=LL|L - L'| = |(L - f(x)) + (f(x) - L')| \le |L - f(x)| + |f(x) - L'| = |f(x) - L| + |f(x) - L'| < \varepsilon + \varepsilon = 2\varepsilon = |L - L'|.

step 5.1L3L4L5
7.1

So LL<LL|L - L'| < |L - L'|, which trichotomy forbids; the assumption LLL \ne L' is untenable, and hence L=LL = L'.

step 6.1L5discharge-contradiction

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

The limit at cc depends only on the restriction of ff to a punctured neighbourhood of cc, and passes to any subset of the domain having cc as a limit point

Statement

Let ARA \subseteq \mathbb{R} and let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}).

  1. Locality. Let f,g:ARf, g : A \to \mathbb{R} and LRL \in \mathbb{R}, and suppose there is a real η>0\eta > 0 with f(x)=g(x)f(x) = g(x) for every xAx \in A satisfying 0<xc<η0 < |x - c| < \eta. Then limxcf(x)=L    limxcg(x)=L\lim_{x \to c} f(x) = L \iff \lim_{x \to c} g(x) = L (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

  2. Restriction. Let BAB \subseteq A with cc a limit point of BB, let f:ARf : A \to \mathbb{R} and suppose limxcf(x)=L\lim_{x \to c} f(x) = L. Then cc is a limit point of AA as well, and limxcfB(x)=L\lim_{x \to c} f|_B(x) = L, where fB:BRf|_B : B \to \mathbb{R} is the restriction of ff.

So the limit at cc sees only the values of ff on an arbitrarily small punctured neighbourhood of cc, and it survives shrinking the domain, provided the smaller domain still accumulates at cc. 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 cc 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 ARA \subseteq \mathbb{R} and a limit point cc of AA; for claim 1 functions f,g:ARf, g : A \to \mathbb{R}, a real LL and a real η>0\eta > 0 with f(x)=g(x)f(x) = g(x) for every xAx \in A satisfying 0<xc<η0 < |x - c| < \eta; for claim 2 a subset BAB \subseteq A having cc as a limit point, a function f:ARf : A \to \mathbb{R} and a real LL with limxcf(x)=L\lim_{x \to c} f(x) = L (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA, Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}).

[L1]

The limit condition: limxch(x)=L\lim_{x \to c} h(x) = L means that for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xx in the domain of hh with 0<xc<δ0 < |x - c| < \delta satisfies h(x)L<ε|h(x) - L| < \varepsilon (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

[L2]

Limit point: cc is a limit point of a set SS when for every real δ>0\delta > 0 there is xSx \in S with 0<xc<δ0 < |x - c| < \delta (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L3]

Order arithmetic: of two positive reals the smaller is positive, the order being total; and u<vwu < v \le w gives u<wu < w (Ordered field).

[L4]

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

technique · direct
1.1

For claim 1, assume limxcf(x)=L\lim_{x \to c} f(x) = L and let ε>0\varepsilon > 0 be an arbitrary real.

assume-hypL1
1.2

For claim 2, BAB \subseteq A and cc is a limit point of BB; hence cc is a limit point of AA, since for every real δ>0\delta > 0 a point xBx \in B with 0<xc<δ0 < |x - c| < \delta is also a point of AA with 0<xc<δ0 < |x - c| < \delta.

L2
1.3

For claim 2, assume limxcf(x)=L\lim_{x \to c} f(x) = L and let ε>0\varepsilon > 0 be an arbitrary real.

assume-hypL1
2.1

By [L1] fix a real δ0>0\delta_0 > 0 such that every xAx \in A with 0<xc<δ00 < |x - c| < \delta_0 satisfies f(x)L<ε|f(x) - L| < \varepsilon, and put δ\delta to be the smaller of δ0\delta_0 and η\eta, so δ>0\delta > 0.

step 1.1L1L3choose
2.2

By [L1] fix a real δ>0\delta > 0 such that every xAx \in A with 0<xc<δ0 < |x - c| < \delta satisfies f(x)L<ε|f(x) - L| < \varepsilon.

step 1.3L1choose
3.1

Every xAx \in A with 0<xc<δ0 < |x - c| < \delta satisfies both 0<xc<δ00 < |x - c| < \delta_0 and 0<xc<η0 < |x - c| < \eta, so g(x)=f(x)g(x) = f(x) and g(x)L=f(x)L<ε|g(x) - L| = |f(x) - L| < \varepsilon; as ε>0\varepsilon > 0 was arbitrary, limxcg(x)=L\lim_{x \to c} g(x) = L.

step 2.1L1L3L4
3.2

Every xBx \in B with 0<xc<δ0 < |x - c| < \delta lies in AA and satisfies 0<xc<δ0 < |x - c| < \delta, so fB(x)=f(x)f|_B(x) = f(x) and therefore f(x)L<ε|f(x) - L| < \varepsilon; as ε>0\varepsilon > 0 was arbitrary, and cc is a limit point of BB, limxcfB(x)=L\lim_{x \to c} f|_B(x) = L.

step 2.2L1L4
4.1

The hypothesis of claim 1 is symmetric in ff and gg, 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.

step 1.2step 3.1step 3.2

Remarks

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

The left and right limits of ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty)

Definition

Let ARA \subseteq \mathbb{R}, let f:ARf : A \to \mathbb{R} and let cRc \in \mathbb{R}. Put

A:=A(,c),A+:=A(c,)A^{-} := A \cap (-\infty, c), \qquad A^{+} := A \cap (c, \infty)

(Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length), and write f:=fAf^{-} := f|_{A^{-}} and f+:=fA+f^{+} := f|_{A^{+}} for the restrictions of ff to those sets.

Right limit. Suppose cc is a limit point of A+A^{+} (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}). For LRL \in \mathbb{R} we write

limxc+f(x)=L:limxcf+(x)=L\lim_{x \to c^{+}} f(x) = L \quad :\Longleftrightarrow \quad \lim_{x \to c} f^{+}(x) = L

in the sense of The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA. Written out: for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that

f(x)L<εfor every xA with c<x<c+δ.|f(x) - L| < \varepsilon \qquad \text{for every } x \in A \text{ with } c < x < c + \delta .

Left limit. Suppose cc is a limit point of AA^{-}. For LRL \in \mathbb{R} we write limxcf(x)=L\lim_{x \to c^{-}} f(x) = L when limxcf(x)=L\lim_{x \to c} f^{-}(x) = L; written out, for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 with f(x)L<ε|f(x) - L| < \varepsilon for every xAx \in A with cδ<x<cc - \delta < x < c.

The written-out forms agree with the definitions. For xA+x \in A^{+} the two conditions 0<xc<δ0 < |x - c| < \delta and c<x<c+δc < x < c + \delta are the same: x>cx > c gives xc>0x - c > 0, so xc=xc|x - c| = x - c and 0<xc<δ0 < |x - c| < \delta reads 0<xc<δ0 < x - c < \delta (Basic properties of the absolute value). Symmetrically on the left, where x<cx < c gives xc=cx|x - c| = c - x.

Well-posedness is inherited, not reproved. A one-sided limit is a limit, namely the limit of a restriction, so:

When the symbols are defined. If cc is not a limit point of A+A^{+} — for instance if AA contains no point to the right of cc, or only points bounded away from cc on that side — then limxc+f(x)\lim_{x \to c^{+}} f(x) is not defined here, for the reason given in The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA: the ε\varepsilon-δ\delta condition would be satisfied vacuously by every real at once. The same applies on the left.

Remarks

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

Limits at ++\infty and -\infty, and infinite limits at a point

Definition

Throughout, ++\infty and -\infty are abbreviations and not real numbers, exactly as in Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length and Divergence to ++\infty and to -\infty. Every phrase below is a single abbreviation for a displayed condition on reals, and no arithmetic is ever performed with the symbols.

Limits at ++\infty. Let ARA \subseteq \mathbb{R} be not bounded above (Lower bound, bounded below, bounded set), let f:ARf : A \to \mathbb{R} and let LRL \in \mathbb{R}. We write

limx+f(x)=L\lim_{x \to +\infty} f(x) = L

when for every real ε>0\varepsilon > 0 there is a real MM such that

f(x)L<εfor every xA with x>M.|f(x) - L| < \varepsilon \qquad \text{for every } x \in A \text{ with } x > M .

Limits at -\infty. Let AA be not bounded below. We write limxf(x)=L\lim_{x \to -\infty} f(x) = L when for every real ε>0\varepsilon > 0 there is a real MM with f(x)L<ε|f(x) - L| < \varepsilon for every xAx \in A with x<Mx < M.

Why unboundedness is required. It plays exactly the role the limit-point condition plays in The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA. Saying that AA is not bounded above says that no real is an upper bound of AA, that is, that for every real MM there is xAx \in A with x>Mx > M (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 LL would satisfy it and the notation would not denote.

Uniqueness, proved here. Suppose AA is not bounded above and limx+f(x)=L\lim_{x \to +\infty} f(x) = L and limx+f(x)=L\lim_{x \to +\infty} f(x) = L' with LLL \ne L'. Then LL>0|L - L'| > 0 (Basic properties of the absolute value), so ε:=LL/2>0\varepsilon := |L - L'|/2 > 0 (The multiplicative identity is positive, Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication). Choose reals M1,M2M_1, M_2 witnessing the two conditions at this ε\varepsilon and let MM be the larger of them, the order being total. Since AA is not bounded above there is xAx \in A with x>Mx > M, hence with x>M1x > M_1 and x>M2x > M_2, and then

LL=(Lf(x))+(f(x)L)f(x)L+f(x)L<2ε=LL|L - L'| = |(L - f(x)) + (f(x) - L')| \le |f(x) - L| + |f(x) - L'| < 2\varepsilon = |L - L'|

(The triangle inequality, Basic properties of the absolute value, Order is preserved by adding a constant and by adding inequalities), which trichotomy forbids. So L=LL = L', and the notation limx+f(x)\lim_{x \to +\infty} f(x) denotes a single real. The same four lines, with the inequalities on xx reversed, give uniqueness at -\infty.

Infinite limits at a point. Let ARA \subseteq \mathbb{R}, let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}) and let f:ARf : A \to \mathbb{R}. We write

f(x)+  as  xcf(x) \to +\infty \ \text{ as } \ x \to c

when for every real MM there is a real δ>0\delta > 0 such that f(x)>Mf(x) > M for every xAx \in A with 0<xc<δ0 < |x - c| < \delta; and f(x)f(x) \to -\infty as xcx \to c when for every real MM there is a real δ>0\delta > 0 with f(x)<Mf(x) < M for every such xx.

This library does not write limxcf(x)=+\lim_{x \to c} f(x) = +\infty. The right-hand side would not be an element of R\mathbb{R}, 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 ++\infty and to -\infty for sequences and by Conventions: sup\sup \emptyset, 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 ±\pm\infty.

Combined forms. Let AA be not bounded above and f:ARf : A \to \mathbb{R}. We write f(x)+f(x) \to +\infty as x+x \to +\infty when for every real NN there is a real MM with f(x)>Nf(x) > N for every xAx \in A with x>Mx > M. The other forms are obtained the same way, by pairing one of the two conditions on xx (unbounded above, unbounded below) with one of the two conditions on f(x)f(x) (above every real, below every real); each is again a single abbreviation for the displayed condition, and none of them is an equation.

Remarks

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)Open item page →

Heine criterion: limxcf(x)=L\lim_{x \to c} f(x) = L iff f(xk)Lf(x_k) \to L for every sequence in A{c}A \setminus \{c\} converging to cc

Statement

Let ARA \subseteq \mathbb{R}, let f:ARf : A \to \mathbb{R}, let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}) and let LRL \in \mathbb{R}. The following are equivalent.

  1. limxcf(x)=L\lim_{x \to c} f(x) = L (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).
  2. For every sequence (xk)kN(x_k)_{k \in \mathbb{N}} with xkAx_k \in A and xkcx_k \ne c for every kk, and xkcx_k \to c (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals), the sequence (f(xk))kN(f(x_k))_{k \in \mathbb{N}} converges to LL.

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 (ACω\mathrm{AC}_\omega)) 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-ε\varepsilon direction of the Heine criterion uses countable choice for R\mathbb{R}, and where this library records that cost; the same asymmetry appears, for the same reason, in A point lies in the closure of ARA \subseteq \mathbb{R} iff some sequence in AA converges to it, so a subset of R\mathbb{R} is closed iff it is sequentially closed.

Because of this, the results on this page that can be proved directly from ε\varepsilon and δ\delta — 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 cc as soon as two sequences in A{c}A \setminus \{c\} tending to cc give different limits of the values, which needs only the choice-free direction.

Facts & Assumptions

Given: A set ARA \subseteq \mathbb{R}, a function f:ARf : A \to \mathbb{R}, a limit point cc of AA and a real LL. Sequences are functions on N\mathbb{N}, and N\mathbb{N} contains 00 (Sequences of reals: bounded, eventually, frequently, tails, subsequences, The natural numbers N\mathbb{N} (von Neumann)), so the shrinking radii used below are 1/(k+1)1/(k+1) and never 1/k1/k.

[L1]

The function limit: limxcf(x)=L\lim_{x \to c} f(x) = L means that for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xAx \in A with 0<xc<δ0 < |x - c| < \delta satisfies f(x)L<ε|f(x) - L| < \varepsilon (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

[L2]

Sequential convergence: (yk)y(y_k) \to y means that for every rational ε>0\varepsilon > 0 there is KNK \in \mathbb{N} with yky<ε|y_k - y| < \varepsilon for all kKk \ge K (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences). Testing instead against every positive REAL ε\varepsilon 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.

[L3]

Limit point: for every real δ>0\delta > 0 there is xAx \in A with 0<xc<δ0 < |x - c| < \delta (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L4]

Reciprocal Archimedean property: for every real ε>0\varepsilon > 0 there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon (For every ε>0\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon, Every complete ordered field is Archimedean); the canonical naturals satisfy n1R>0n \cdot 1_{\mathbb{R}} > 0 and are strictly increasing in nn (Canonical naturals are positive and strictly increasing); and 0<a<b0 < a < b gives 0<1/b<1/a0 < 1/b < 1/a (Inverses of positives are positive, and reciprocation reverses order).

[L5]

Countable choice: for every family (Xk)kN(X_k)_{k \in \mathbb{N}} of nonempty sets there is a function kxkk \mapsto x_k with xkXkx_k \in X_k for every kk (The Axiom of Countable Choice (ACω\mathrm{AC}_\omega)).

[L6]

Absolute value (Basic properties of the absolute value); and trichotomy, so the negation of u<ε|u| < \varepsilon is uε|u| \ge \varepsilon, and the negation of "for every ε\varepsilon there is δ\delta such that P" is "there is ε0\varepsilon_0 such that for every δ\delta, not P" (Ordered field).

Proof

technique · direct
1.1

Assume condition 1, let (xk)(x_k) be a sequence with xkAx_k \in A and xkcx_k \ne c for every kk and xkcx_k \to c, and let ε>0\varepsilon > 0 be an arbitrary real.

assume-hypL1L2L3
1.2

Assume condition 1 FAILS. Negating the quantifiers of [L1], there is a real ε0>0\varepsilon_0 > 0 such that for every real δ>0\delta > 0 some xAx \in A has 0<xc<δ0 < |x - c| < \delta and f(x)Lε0|f(x) - L| \ge \varepsilon_0.

assume-hypL1L6
2.1

By [L1] fix a real δ>0\delta > 0 such that every xAx \in A with 0<xc<δ0 < |x - c| < \delta satisfies f(x)L<ε|f(x) - L| < \varepsilon; and by [L2], δ\delta being a positive real, fix KNK \in \mathbb{N} with xkc<δ|x_k - c| < \delta for every kKk \ge K.

step 1.1L1L2choose
2.2

For kNk \in \mathbb{N} put Xk:={xA : 0<xc<1/(k+1)  and  f(x)Lε0}X_k := \{\, x \in A \ : \ 0 < |x - c| < 1/(k+1) \ \text{ and } \ |f(x) - L| \ge \varepsilon_0 \,\}. Each XkX_k is nonempty, since k+11k + 1 \ge 1 makes 1/(k+1)1/(k+1) a positive real and step 1.2 applies to that radius.

step 1.2L4L6
3.1

For every kKk \ge K we have xkAx_k \in A and xkcx_k \ne c, so 0<xkc<δ0 < |x_k - c| < \delta and hence f(xk)L<ε|f(x_k) - L| < \varepsilon. Since ε>0\varepsilon > 0 was an arbitrary real, f(xk)Lf(x_k) \to L; condition 1 therefore implies condition 2.

step 2.1L1L2L6
3.2

By countable choice applied to the family (Xk)kN(X_k)_{k \in \mathbb{N}}, fix a function kxkk \mapsto x_k with xkXkx_k \in X_k for every kNk \in \mathbb{N}.

step 2.2L5choose
4.1

That sequence has xkAx_k \in A and xkcx_k \ne c for every kk, and it converges to cc: given a real ε>0\varepsilon > 0, [L4] supplies a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon, and every knk \ge n has k+1>n1k + 1 > n \ge 1, hence xkc<1/(k+1)<1/n<ε|x_k - c| < 1/(k+1) < 1/n < \varepsilon.

step 3.2L2L4L6
4.2

Yet (f(xk))(f(x_k)) does not converge to LL: every kk has f(xk)Lε0|f(x_k) - L| \ge \varepsilon_0, while a rational ε\varepsilon with 0<ε<ε00 < \varepsilon < \varepsilon_0 ([L2]) would require some KK with f(xk)L<ε<ε0|f(x_k) - L| < \varepsilon < \varepsilon_0 for all kKk \ge K.

step 3.2L2L6
5.1

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.

step 3.1step 4.1step 4.2

Remarks

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

A function has no limit at cc as soon as two sequences in A{c}A \setminus \{c\} tending to cc give different limits of the values

Statement

Let ARA \subseteq \mathbb{R}, let f:ARf : A \to \mathbb{R} and let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}). Then ff has no limit at cc — that is, no LRL \in \mathbb{R} satisfies limxcf(x)=L\lim_{x \to c} f(x) = L (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA) — as soon as either of the following occurs.

  1. There are sequences (xk)(x_k) and (yk)(y_k) with all terms in A{c}A \setminus \{c\}, both converging to cc, and reals PQP \ne Q with f(xk)Pf(x_k) \to P and f(yk)Qf(y_k) \to Q (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).
  2. There is a sequence (xk)(x_k) with all terms in A{c}A \setminus \{c\}, converging to cc, for which (f(xk))(f(x_k)) 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: limxcf(x)=L\lim_{x \to c} f(x) = L iff f(xk)Lf(x_k) \to L for every sequence in A{c}A \setminus \{c\} converging to cc, 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

[L1]

Heine criterion, the direction from the ε\varepsilon-δ\delta limit to sequences: if limxcf(x)=L\lim_{x \to c} f(x) = L then f(zk)Lf(z_k) \to L for every sequence (zk)(z_k) with all terms in A{c}A \setminus \{c\} converging to cc (Heine criterion: limxcf(x)=L\lim_{x \to c} f(x) = L iff f(xk)Lf(x_k) \to L for every sequence in A{c}A \setminus \{c\} converging to cc). That direction is proved without any choice principle.

[L2]

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

technique · contrapositive
1.1

Each of the two claims has the form "hypothesis \Rightarrow ff has no limit at cc"; we prove the contrapositive of each, namely that if some LRL \in \mathbb{R} satisfies limxcf(x)=L\lim_{x \to c} f(x) = L then neither hypothesis can hold.

contrapositive-reduce
1.2

Assume there is LRL \in \mathbb{R} with limxcf(x)=L\lim_{x \to c} f(x) = L.

assume-hyp
2.1

Let (zk)(z_k) be an arbitrary sequence with all terms in A{c}A \setminus \{c\} converging to cc. By [L1], (f(zk))(f(z_k)) converges, with limit LL.

step 1.2L1
3.1

Under hypothesis 1 this applies to (xk)(x_k) and to (yk)(y_k): f(xk)Pf(x_k) \to P and f(xk)Lf(x_k) \to L give P=LP = L by [L2], and likewise Q=LQ = L, so P=QP = Q; hypothesis 1, which asserts PQP \ne Q, therefore fails.

step 2.1L2
3.2

Under hypothesis 2 it applies to (xk)(x_k) and gives that (f(xk))(f(x_k)) converges; hypothesis 2, which asserts that it does not, therefore fails.

step 2.1L2
4.1

So the existence of a limit of ff at cc excludes both hypotheses; contrapositively, either hypothesis excludes the existence of a limit of ff at cc.

step 3.1step 3.2discharge-contrapositive

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)Open item page →

If ff has a finite limit at cc then ff is bounded on some punctured neighbourhood of cc

Statement

Let ARA \subseteq \mathbb{R}, let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}), let f:ARf : A \to \mathbb{R} and suppose the limit of ff at cc exists, say limxcf(x)=L\lim_{x \to c} f(x) = L (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA). Then there are a real δ>0\delta > 0 and a real M0M \ge 0 with

f(x)Mfor every xA with 0<xc<δ;|f(x)| \le M \qquad \text{for every } x \in A \text{ with } 0 < |x - c| < \delta ;

equivalently, the image f(ANδ(c))f\bigl(A \cap N^{*}_{\delta}(c)\bigr) is a bounded subset of R\mathbb{R} (Lower bound, bounded below, bounded set, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}). One may take M=L+1M = |L| + 1.

Only local boundedness follows, never boundedness on AA. A function with a limit at cc may be unbounded on its domain, as FALSE: a function with a limit at cc is bounded on its whole domain records.

Facts & Assumptions

Given: A set ARA \subseteq \mathbb{R}, a limit point cc of AA, a function f:ARf : A \to \mathbb{R} and a real LL with limxcf(x)=L\lim_{x \to c} f(x) = L (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA, Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}).

[L1]

The limit condition: for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xAx \in A with 0<xc<δ0 < |x - c| < \delta satisfies f(x)L<ε|f(x) - L| < \varepsilon (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

[L2]

Absolute value: u0|u| \ge 0; uuu-|u| \le u \le |u|; and for t>0t > 0, ut|u| \le t is equivalent to tut-t \le u \le t (Basic properties of the absolute value).

[L3]

Triangle inequality: u+vu+v|u + v| \le |u| + |v| (The triangle inequality).

[L4]

Order arithmetic: 0<10 < 1 (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 u<vu < v implies uvu \le v. 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).

[L5]

Bounded set: SRS \subseteq \mathbb{R} is bounded when it has both an upper and a lower bound (Lower bound, bounded below, bounded set); and Nδ(c)={y:0<yc<δ}N^{*}_{\delta}(c) = \{\, y : 0 < |y - c| < \delta \,\} (The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

Proof

technique · direct
1.1

Apply [L1] with the particular value ε=1\varepsilon = 1, legitimate since 1>01 > 0: fix a real δ>0\delta > 0 such that every xAx \in A with 0<xc<δ0 < |x - c| < \delta satisfies f(x)L<1|f(x) - L| < 1.

L1L4choose
1.2

Put M:=L+1M := |L| + 1. Then M0M \ge 0, since L0|L| \ge 0 and 1>01 > 0.

L2L4
2.1

For every xAx \in A with 0<xc<δ0 < |x - c| < \delta we have f(x)=(f(x)L)+Lf(x)L+L<1+L=M|f(x)| = |(f(x) - L) + L| \le |f(x) - L| + |L| < 1 + |L| = M, hence f(x)M|f(x)| \le M.

step 1.1step 1.2L2L3L4
3.1

Therefore Mf(x)M-M \le f(x) \le M for every such xx, so MM is an upper bound and M-M a lower bound of the image f(ANδ(c))f\bigl(A \cap N^{*}_{\delta}(c)\bigr): that image is a bounded subset of R\mathbb{R}.

step 2.1L2L5

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

If limxcf(x)=L0\lim_{x \to c} f(x) = L \ne 0 then f>L/2|f| > |L|/2 on a punctured neighbourhood of cc; in particular if L>0L > 0 then f>L/2>0f > L/2 > 0 there

Statement

Let ARA \subseteq \mathbb{R}, let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}), let f:ARf : A \to \mathbb{R} and suppose the limit of ff at cc exists with limxcf(x)=L\lim_{x \to c} f(x) = L and L0L \ne 0 (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA). Then there is a real δ>0\delta > 0 such that every xAx \in A with 0<xc<δ0 < |x - c| < \delta satisfies

f(x)  >  L2  >  0;|f(x)| \;>\; \frac{|L|}{2} \;>\; 0 ;

in particular f(x)0f(x) \ne 0 for every such xx. Moreover:

  • if L>0L > 0 then f(x)>L/2>0f(x) > L/2 > 0 for every such xx;
  • if L<0L < 0 then f(x)<L/2<0f(x) < L/2 < 0 for every such xx.

Consequently, writing

A0:={xA : f(x)0},A_0 := \{\, x \in A \ : \ f(x) \ne 0 \,\},

the point cc is a limit point of A0A_0.

The bound L/2|L|/2, and not merely "f0f \ne 0", 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 1/f1/|f| near cc and therefore needs a positive lower bound on f|f| there, and the last claim is what lets a limit be taken on the smaller domain A0A_0 at all.

Facts & Assumptions

Given: A set ARA \subseteq \mathbb{R}, a limit point cc of AA, a function f:ARf : A \to \mathbb{R} and a real L0L \ne 0 with limxcf(x)=L\lim_{x \to c} f(x) = L; and A0:={xA:f(x)0}A_0 := \{\, x \in A : f(x) \ne 0 \,\} (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA, Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}).

[L1]

The limit condition: for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xAx \in A with 0<xc<δ0 < |x - c| < \delta satisfies f(x)L<ε|f(x) - L| < \varepsilon (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

[L2]

Absolute value: u0|u| \ge 0; u=0|u| = 0 if and only if u=0u = 0; u=u|u| = u for u0u \ge 0 and u=u|u| = -u for u0u \le 0; and for t>0t > 0, u<t|u| < t is equivalent to t<u<t-t < u < t (Basic properties of the absolute value).

[L3]

Reverse triangle inequality: uvuv\bigl| |u| - |v| \bigr| \le |u - v| (The reverse triangle inequality).

[L4]

Limit point: for every real ρ>0\rho > 0 there is xAx \in A with 0<xc<ρ0 < |x - c| < \rho (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L5]

Order arithmetic in R\mathbb{R}: trichotomy, so u0u \ne 0 with u0|u| \ge 0 and u0|u| \ne 0 forces u>0|u| > 0; 0<10 < 1 (The multiplicative identity is positive), hence 2>02 > 0 and 21>02^{-1} > 0 (Inverses of positives are positive, and reciprocation reverses order), so t/2>0t/2 > 0 and tt/2=t/2t - t/2 = t/2 for t>0t > 0 (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

technique · direct
1.1

Since L0L \ne 0 we have L0|L| \ne 0 while L0|L| \ge 0, so trichotomy gives L>0|L| > 0, and ε:=L/2>0\varepsilon := |L|/2 > 0 with LL/2=L/2|L| - |L|/2 = |L|/2.

givenL2L5
2.1

Apply [L1] with this ε\varepsilon: fix a real δ>0\delta > 0 such that every xAx \in A with 0<xc<δ0 < |x - c| < \delta satisfies f(x)L<L/2|f(x) - L| < |L|/2.

step 1.1L1choose
3.1

For every such xx the reverse triangle inequality gives f(x)Lf(x)L<L/2\bigl| |f(x)| - |L| \bigr| \le |f(x) - L| < |L|/2, hence f(x)L>L/2|f(x)| - |L| > -|L|/2 and so f(x)>LL/2=L/2>0|f(x)| > |L| - |L|/2 = |L|/2 > 0; in particular f(x)0|f(x)| \ne 0 and therefore f(x)0f(x) \ne 0.

step 2.1L2L3L5
3.2

If L>0L > 0 then L=L|L| = L, and for every such xx the estimate f(x)L<L/2|f(x) - L| < L/2 gives L/2<f(x)L-L/2 < f(x) - L, that is f(x)>LL/2=L/2>0f(x) > L - L/2 = L/2 > 0.

step 2.1L2L5
3.3

If L<0L < 0 then L=L|L| = -L, and for every such xx the estimate f(x)L<L/2|f(x) - L| < -L/2 gives f(x)L<L/2f(x) - L < -L/2, that is f(x)<LL/2=L/2<0f(x) < L - L/2 = L/2 < 0.

step 2.1L2L5
4.1

Let η>0\eta > 0 be an arbitrary real and let ρ\rho be the smaller of δ\delta and η\eta, so ρ>0\rho > 0. Since cc is a limit point of AA there is xAx \in A with 0<xc<ρ0 < |x - c| < \rho; that xx satisfies 0<xc<δ0 < |x - c| < \delta, hence f(x)0f(x) \ne 0 by step 3.1, so xA0x \in A_0 and 0<xc<η0 < |x - c| < \eta. As η\eta was arbitrary, cc is a limit point of A0A_0.

step 3.1L4L5
5.1

So on ANδ(c)A \cap N^{*}_{\delta}(c) the function is bounded away from 00 by L/2|L|/2 and carries the sign of LL, and cc remains a limit point of the set A0A_0 where ff does not vanish.

step 3.1step 3.2step 3.3step 4.1

Remarks

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero

Statement

Let ARA \subseteq \mathbb{R}, let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}), let f,g:ARf, g : A \to \mathbb{R} and let αR\alpha \in \mathbb{R}. Suppose the limits of ff and of gg at cc exist, and write L:=limxcf(x)L := \lim_{x \to c} f(x) and M:=limxcg(x)M := \lim_{x \to c} g(x) (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA). Then:

  1. the limit of f+gf + g at cc exists, and limxc(f+g)(x)  =  limxcf(x)+limxcg(x)  =  L+M;\lim_{x \to c} (f + g)(x) \;=\; \lim_{x \to c} f(x) + \lim_{x \to c} g(x) \;=\; L + M ;
  2. the limit of αf\alpha f at cc exists, and limxc(αf)(x)  =  αlimxcf(x)  =  αL;\lim_{x \to c} (\alpha f)(x) \;=\; \alpha \lim_{x \to c} f(x) \;=\; \alpha L ;
  3. the limit of fgfg at cc exists, and limxc(fg)(x)  =  (limxcf(x))(limxcg(x))  =  LM;\lim_{x \to c} (fg)(x) \;=\; \Bigl(\lim_{x \to c} f(x)\Bigr)\Bigl(\lim_{x \to c} g(x)\Bigr) \;=\; LM ;
  4. if M0M \ne 0, then, writing A0:={xA:g(x)0}A_0 := \{\, x \in A : g(x) \ne 0 \,\}, the point cc is a limit point of A0A_0, the quotient f/gf/g is defined on A0A_0 by (f/g)(x)=f(x)/g(x)(f/g)(x) = f(x) / g(x), the limit of (f/g)A0(f/g)|_{A_0} at cc exists, and limxc(f/g)A0(x)  =  limxcf(x)limxcg(x)  =  LM.\lim_{x \to c} (f/g)|_{A_0}(x) \;=\; \frac{\lim_{x \to c} f(x)}{\lim_{x \to c} g(x)} \;=\; \frac{L}{M} .

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 ε\varepsilon and δ\delta. No sequence is constructed and no choice principle is used, so all four claims are theorems of ZF. Passing through Heine criterion: limxcf(x)=L\lim_{x \to c} f(x) = L iff f(xk)Lf(x_k) \to L for every sequence in A{c}A \setminus \{c\} converging to cc instead would import the countable choice spent in that theorem's converse direction, for no gain; see The sequence-to-ε\varepsilon direction of the Heine criterion uses countable choice for R\mathbb{R}, and where this library records that cost.

Why the quotient is stated on A0A_0. The function f/gf/g is simply not defined where gg vanishes, and gg may well vanish at points of AA arbitrarily far from cc; restricting to A0A_0 is therefore forced. That this restriction still has cc as a limit point, so that the limit there means anything at all, is the last claim of If limxcf(x)=L0\lim_{x \to c} f(x) = L \ne 0 then f>L/2|f| > |L|/2 on a punctured neighbourhood of cc; in particular if L>0L > 0 then f>L/2>0f > L/2 > 0 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 ARA \subseteq \mathbb{R}, a limit point cc of AA, functions f,g:ARf, g : A \to \mathbb{R}, a real α\alpha, and reals L,ML, M with limxcf(x)=L\lim_{x \to c} f(x) = L and limxcg(x)=M\lim_{x \to c} g(x) = M; for claim 4 also M0M \ne 0 and A0:={xA:g(x)0}A_0 := \{\, x \in A : g(x) \ne 0 \,\} (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA, Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}).

[L1]

The limit condition: limxch(x)=P\lim_{x \to c} h(x) = P means that for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xx in the domain of hh with 0<xc<δ0 < |x - c| < \delta satisfies h(x)P<ε|h(x) - P| < \varepsilon (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

[L2]

Absolute value: u0|u| \ge 0; u=0|u| = 0 if and only if u=0u = 0; uv=uv|uv| = |u|\,|v|; and u=u|{-u}| = |u| (Basic properties of the absolute value).

[L3]

Triangle inequality: u+vu+v|u + v| \le |u| + |v| (The triangle inequality).

[L4]

Order and field arithmetic in R\mathbb{R}: adding two strict inequalities (Order is preserved by adding a constant and by adding inequalities); for t>0t > 0, u<vu < v is equivalent to ut<vtut < vt, and 0uv0 \le u \le v with 0st0 \le s \le t gives usvtus \le vt (Sign rules for products and monotonicity of multiplication); positive elements have positive inverses and 0<a<b0 < a < b gives 0<1/b<1/a0 < 1/b < 1/a (Inverses of positives are positive, and reciprocation reverses order); 0<10 < 1 (The multiplicative identity is positive), so 2>02 > 0 and t/2>0t/2 > 0 for t>0t > 0; inverses and the field identities (Field); trichotomy and totality, so of finitely many positive reals the smallest is positive (Ordered field).

[L5]

Local boundedness: there are a real δ0>0\delta_0 > 0 and a real K0K \ge 0 with f(x)K|f(x)| \le K for every xAx \in A satisfying 0<xc<δ00 < |x - c| < \delta_0 (If ff has a finite limit at cc then ff is bounded on some punctured neighbourhood of cc).

[L6]

Sign preservation: if M0M \ne 0 there is a real δs>0\delta_s > 0 with g(x)>M/2>0|g(x)| > |M|/2 > 0 for every xAx \in A satisfying 0<xc<δs0 < |x - c| < \delta_s, and cc is a limit point of A0A_0 (If limxcf(x)=L0\lim_{x \to c} f(x) = L \ne 0 then f>L/2|f| > |L|/2 on a punctured neighbourhood of cc; in particular if L>0L > 0 then f>L/2>0f > L/2 > 0 there).

[L7]

Restriction: if BAB \subseteq A has cc as a limit point and limxcf(x)=L\lim_{x \to c} f(x) = L, then limxcfB(x)=L\lim_{x \to c} f|_B(x) = L (claim 2 of The limit at cc depends only on the restriction of ff to a punctured neighbourhood of cc, and passes to any subset of the domain having cc as a limit point).

Proof

technique · direct
1.1

Sum. Let ε>0\varepsilon > 0 be an arbitrary real. By [L1] fix reals δ1,δ2>0\delta_1, \delta_2 > 0 with f(x)L<ε/2|f(x) - L| < \varepsilon/2 for every xAx \in A satisfying 0<xc<δ10 < |x - c| < \delta_1 and g(x)M<ε/2|g(x) - M| < \varepsilon/2 for every xAx \in A satisfying 0<xc<δ20 < |x - c| < \delta_2, and let δ\delta be the smaller of the two, so δ>0\delta > 0. For xAx \in A with 0<xc<δ0 < |x - c| < \delta we get (f+g)(x)(L+M)=(f(x)L)+(g(x)M)f(x)L+g(x)M<ε|(f+g)(x) - (L+M)| = |(f(x) - L) + (g(x) - M)| \le |f(x) - L| + |g(x) - M| < \varepsilon. As ε\varepsilon was arbitrary, the limit of f+gf + g at cc exists and equals L+ML + M: claim 1.

L1L2L3L4choose
1.2

Scalar multiple. If α=0\alpha = 0 then αf\alpha f is the constant function 00 and αL=0\alpha L = 0, so (αf)(x)αL=0<ε|(\alpha f)(x) - \alpha L| = 0 < \varepsilon for every xx and every ε>0\varepsilon > 0, any δ\delta serving. If α0\alpha \ne 0 then α>0|\alpha| > 0; given a real ε>0\varepsilon > 0, [L1] supplies δ>0\delta > 0 with f(x)L<ε/α|f(x) - L| < \varepsilon/|\alpha| on ANδ(c)A \cap N^{*}_{\delta}(c), and there (αf)(x)αL=αf(x)L<ε|(\alpha f)(x) - \alpha L| = |\alpha|\,|f(x) - L| < \varepsilon. So the limit of αf\alpha f at cc exists and equals αL\alpha L: claim 2.

L1L2L4L8choose
1.3

A working bound for ff near cc. By [L5] fix a real δ0>0\delta_0 > 0 and a real K0K \ge 0 with f(x)K|f(x)| \le K for every xAx \in A satisfying 0<xc<δ00 < |x - c| < \delta_0, and put K:=K+1K' := K + 1, so K>0K' > 0 and f(x)K|f(x)| \le K' for all those xx.

L4L5choose
1.4

The denominator near cc. Assume M0M \ne 0. By [L6] fix a real δs>0\delta_s > 0 with g(x)>M/2>0|g(x)| > |M|/2 > 0 for every xAx \in A satisfying 0<xc<δs0 < |x - c| < \delta_s; every such xx has g(x)0g(x) \ne 0, hence lies in A0A_0, and cc is a limit point of A0A_0.

L2L4L6
2.1

Product. Let ε>0\varepsilon > 0 be an arbitrary real. By [L1] fix reals δ1,δ2>0\delta_1, \delta_2 > 0 with g(x)M<ε/(2K)|g(x) - M| < \varepsilon/(2K') on ANδ1(c)A \cap N^{*}_{\delta_1}(c) and f(x)L<ε/(2(M+1))|f(x) - L| < \varepsilon / \bigl(2(|M| + 1)\bigr) on ANδ2(c)A \cap N^{*}_{\delta_2}(c), and let δ\delta be the smallest of δ0,δ1,δ2\delta_0, \delta_1, \delta_2, which is positive. For xAx \in A with 0<xc<δ0 < |x - c| < \delta, f(x)g(x)LM=f(x)(g(x)M)+M(f(x)L)f(x)g(x)M+Mf(x)LKg(x)M+(M+1)f(x)L<ε/2+ε/2=ε|f(x)g(x) - LM| = |f(x)(g(x) - M) + M(f(x) - L)| \le |f(x)|\,|g(x) - M| + |M|\,|f(x) - L| \le K'\,|g(x) - M| + (|M|+1)\,|f(x) - L| < \varepsilon/2 + \varepsilon/2 = \varepsilon. As ε\varepsilon was arbitrary, the limit of fgfg at cc exists and equals LMLM: claim 3.

step 1.3L1L2L3L4L8choose
2.2

Reciprocal. Assume M0M \ne 0 and let ε>0\varepsilon > 0 be an arbitrary real. By [L1] fix a real δ3>0\delta_3 > 0 with g(x)M<εM2/2|g(x) - M| < \varepsilon |M|^2 / 2 on ANδ3(c)A \cap N^{*}_{\delta_3}(c), and let δ\delta be the smaller of δs\delta_s and δ3\delta_3. For xA0x \in A_0 with 0<xc<δ0 < |x - c| < \delta we have g(x)>M/2>0|g(x)| > |M|/2 > 0, hence g(x)M>M2/2>0|g(x)|\,|M| > |M|^2/2 > 0 and so 1/(g(x)M)<2/M21/(|g(x)|\,|M|) < 2/|M|^2; therefore 1/g(x)1/M=Mg(x)/(g(x)M)<(εM2/2)(2/M2)=ε\bigl| 1/g(x) - 1/M \bigr| = |M - g(x)| \big/ \bigl(|g(x)|\,|M|\bigr) < (\varepsilon |M|^2/2)\cdot(2/|M|^2) = \varepsilon. As ε\varepsilon was arbitrary, the limit of (1/g)A0(1/g)|_{A_0} at cc exists and equals 1/M1/M.

step 1.4L1L2L4L8choose
2.3

The numerator on the smaller domain. Assume M0M \ne 0. Since A0AA_0 \subseteq A and cc is a limit point of A0A_0 by step 1.4, [L7] gives that the limit of fA0f|_{A_0} at cc exists and equals LL.

step 1.4L7
3.1

Quotient. Assume M0M \ne 0. On the domain A0A_0, which has cc as a limit point, the two functions fA0f|_{A_0} and (1/g)A0(1/g)|_{A_0} have limits LL and 1/M1/M at cc by steps 2.3 and 2.2, and their product is (f/g)A0(f/g)|_{A_0} by the field identities; so claim 3, applied on the domain A0A_0, gives that the limit of (f/g)A0(f/g)|_{A_0} at cc exists and equals L(1/M)=L/ML \cdot (1/M) = L/M.

step 2.1step 2.2step 2.3L2L4
4.1

Claims 1 to 4 are proved, each directly from the ε\varepsilon-δ\delta definition and none of them through a sequence.

step 1.1step 1.2step 2.1step 3.1

Remarks

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

If fgf \le g on a punctured neighbourhood of cc then limflimg\lim f \le \lim g, non-strictly

Statement

Let ARA \subseteq \mathbb{R}, let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}), let f,g:ARf, g : A \to \mathbb{R} and suppose both limits at cc exist (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA). Suppose further that there is a real η>0\eta > 0 with

f(x)g(x)for every xA with 0<xc<η.f(x) \le g(x) \qquad \text{for every } x \in A \text{ with } 0 < |x - c| < \eta .

Then

limxcf(x)    limxcg(x).\lim_{x \to c} f(x) \;\le\; \lim_{x \to c} g(x) .

The conclusion is non-strict even when the hypothesis is strict. Replacing \le by << on both sides gives a false statement, refuted by FALSE: f<gf < g near cc implies limf<limg\lim f < \lim g: strictness is destroyed in the limit, and no hypothesis short of a uniform gap restores it.

Only the values near cc matter, by The limit at cc depends only on the restriction of ff to a punctured neighbourhood of cc, and passes to any subset of the domain having cc as a limit point: the hypothesis is imposed on a punctured neighbourhood of cc and on nothing else, and it says nothing about f(c)f(c) and g(c)g(c), which the definition ignores in any case.

Facts & Assumptions

Given: A set ARA \subseteq \mathbb{R}, a limit point cc of AA, functions f,g:ARf, g : A \to \mathbb{R}, reals L,ML, M with limxcf(x)=L\lim_{x \to c} f(x) = L and limxcg(x)=M\lim_{x \to c} g(x) = M, and a real η>0\eta > 0 with f(x)g(x)f(x) \le g(x) for every xAx \in A satisfying 0<xc<η0 < |x - c| < \eta (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA, Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}).

[L1]

The limit condition: for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xAx \in A with 0<xc<δ0 < |x - c| < \delta satisfies f(x)L<ε|f(x) - L| < \varepsilon, and likewise for gg and MM (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

[L2]

Limit point: for every real ρ>0\rho > 0 there is xAx \in A with 0<xc<ρ0 < |x - c| < \rho (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L3]

Absolute value: for t>0t > 0, u<t|u| < t is equivalent to t<u<t-t < u < t (Basic properties of the absolute value).

[L4]

Order arithmetic in R\mathbb{R}: the order is total, so the negation of uvu \le v is v<uv < u; trichotomy, so u<vu < v and vuv \le u cannot both hold; adding a constant to an inequality and adding two inequalities (Order is preserved by adding a constant and by adding inequalities); 0<10 < 1 (The multiplicative identity is positive), so 2>02 > 0, 21>02^{-1} > 0 (Inverses of positives are positive, and reciprocation reverses order) and t/2>0t/2 > 0 for t>0t > 0 (Sign rules for products and monotonicity of multiplication), with (t/2)+(t/2)=t(t/2) + (t/2) = t; and of finitely many positive reals the smallest is positive (Ordered field).

Proof

technique · contradiction
1.1

Suppose, for contradiction, that LML \le M fails; the order being total, this means M<LM < L.

assume-contra
2.1

Then LM>0L - M > 0, so ε:=(LM)/2>0\varepsilon := (L - M)/2 > 0, and Lε=(L+M)/2=M+εL - \varepsilon = (L + M)/2 = M + \varepsilon.

step 1.1L4
3.1

By [L1] fix reals δ1,δ2>0\delta_1, \delta_2 > 0 such that every xAx \in A with 0<xc<δ10 < |x - c| < \delta_1 has f(x)L<ε|f(x) - L| < \varepsilon and every xAx \in A with 0<xc<δ20 < |x - c| < \delta_2 has g(x)M<ε|g(x) - M| < \varepsilon; let δ\delta be the smallest of δ1\delta_1, δ2\delta_2 and η\eta, so δ>0\delta > 0.

step 2.1L1L4choose
4.1

Since cc is a limit point of AA, fix xAx \in A with 0<xc<δ0 < |x - c| < \delta.

step 3.1L2choose
5.1

That xx satisfies 0<xc<δ10 < |x - c| < \delta_1 and 0<xc<δ20 < |x - c| < \delta_2, so f(x)L<ε|f(x) - L| < \varepsilon gives f(x)>Lεf(x) > L - \varepsilon and g(x)M<ε|g(x) - M| < \varepsilon gives g(x)<M+εg(x) < M + \varepsilon; since Lε=M+εL - \varepsilon = M + \varepsilon, this yields g(x)<f(x)g(x) < f(x).

step 3.1step 4.1L3L4
6.1

But that same xx satisfies 0<xc<η0 < |x - c| < \eta, so the hypothesis gives f(x)g(x)f(x) \le g(x), which together with g(x)<f(x)g(x) < f(x) contradicts trichotomy.

step 3.1step 5.1L4
7.1

The assumption that LML \le M fails is therefore untenable, and limxcf(x)=LM=limxcg(x)\lim_{x \to c} f(x) = L \le M = \lim_{x \to c} g(x).

step 6.1L4discharge-contradiction

Remarks

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

If fghf \le g \le h near cc and ff and hh have the same limit at cc, then so does gg

Statement

Let ARA \subseteq \mathbb{R}, let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}) and let f,g,h:ARf, g, h : A \to \mathbb{R}. Suppose there is a real η>0\eta > 0 with

f(x)g(x)h(x)for every xA with 0<xc<η,f(x) \le g(x) \le h(x) \qquad \text{for every } x \in A \text{ with } 0 < |x - c| < \eta ,

and suppose the limits of ff and of hh at cc exist and are equal, say limxcf(x)=limxch(x)=L\lim_{x \to c} f(x) = \lim_{x \to c} h(x) = L (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA). Then the limit of gg at cc exists, and

limxcg(x)  =  limxcf(x)  =  limxch(x)  =  L.\lim_{x \to c} g(x) \;=\; \lim_{x \to c} f(x) \;=\; \lim_{x \to c} h(x) \;=\; L .

This is the one result on this page that produces a limit rather than computing one. No hypothesis whatever is placed on gg beyond the two inequalities: gg may be wildly irregular, as xxψ(1/x)x \mapsto x\,\psi(1/x) on the companion page is, and the theorem still delivers its limit at cc.

The proof is a direct ε\varepsilon-δ\delta argument and uses no choice principle.

Facts & Assumptions

Given: A set ARA \subseteq \mathbb{R}, a limit point cc of AA, functions f,g,h:ARf, g, h : A \to \mathbb{R}, a real η>0\eta > 0 with f(x)g(x)h(x)f(x) \le g(x) \le h(x) for every xAx \in A satisfying 0<xc<η0 < |x - c| < \eta, and a real LL with limxcf(x)=L\lim_{x \to c} f(x) = L and limxch(x)=L\lim_{x \to c} h(x) = L (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA, Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}).

[L1]

The limit condition: for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xAx \in A with 0<xc<δ0 < |x - c| < \delta satisfies f(x)L<ε|f(x) - L| < \varepsilon, and likewise for hh (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

[L2]

Absolute value: for t>0t > 0, u<t|u| < t is equivalent to t<u<t-t < u < t (Basic properties of the absolute value).

[L3]

Order arithmetic in R\mathbb{R}: the order is transitive, and mixed chains compose, so u<vwu < v \le w gives u<wu < w and uv<wu \le v < w gives u<wu < w; 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).

[L4]

Neighbourhoods: Nδ(c)={y:0<yc<δ}N^{*}_{\delta}(c) = \{\, y : 0 < |y - c| < \delta \,\}, and a smaller radius gives a smaller punctured neighbourhood (The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

Proof

technique · direct
1.1

Let ε>0\varepsilon > 0 be an arbitrary real. By [L1] fix reals δ1,δ2>0\delta_1, \delta_2 > 0 such that every xAx \in A with 0<xc<δ10 < |x - c| < \delta_1 satisfies f(x)L<ε|f(x) - L| < \varepsilon and every xAx \in A with 0<xc<δ20 < |x - c| < \delta_2 satisfies h(x)L<ε|h(x) - L| < \varepsilon; let δ\delta be the smallest of δ1\delta_1, δ2\delta_2 and η\eta, so δ>0\delta > 0.

L1L3L4choose
2.1

Let xAx \in A with 0<xc<δ0 < |x - c| < \delta. Then 0<xc<δ10 < |x - c| < \delta_1 gives Lε<f(x)L - \varepsilon < f(x), and 0<xc<δ20 < |x - c| < \delta_2 gives h(x)<L+εh(x) < L + \varepsilon, while 0<xc<η0 < |x - c| < \eta gives f(x)g(x)h(x)f(x) \le g(x) \le h(x).

step 1.1L2L3L4
3.1

Chaining those four inequalities, Lε<f(x)g(x)h(x)<L+εL - \varepsilon < f(x) \le g(x) \le h(x) < L + \varepsilon, hence Lε<g(x)<L+εL - \varepsilon < g(x) < L + \varepsilon, that is ε<g(x)L<ε-\varepsilon < g(x) - L < \varepsilon, that is g(x)L<ε|g(x) - L| < \varepsilon.

step 2.1L2L3
4.1

So for every real ε>0\varepsilon > 0 a real δ>0\delta > 0 has been produced with g(x)L<ε|g(x) - L| < \varepsilon for every xAx \in A satisfying 0<xc<δ0 < |x - c| < \delta: the limit of gg at cc exists and equals LL.

step 3.1L1

Remarks

  • Where the three hypotheses are spent. The inequality fgf \le g is used only for the lower estimate and ghg \le h only for the upper one; the equality of the two outer limits is what makes the two estimates close on the same number LL. Drop it and the argument gives only limflim inf\lim f \le \liminf-style information, which this page does not develop.

  • The order hypothesis is local. It is imposed only on ANη(c)A \cap N^{*}_{\eta}(c), so the theorem is insensitive to the behaviour of the three functions far from cc, and to their values at cc; that is The limit at cc depends only on the restriction of ff to a punctured neighbourhood of cc, and passes to any subset of the domain having cc as a limit point in action.

  • Typical use. To prove that a bounded oscillating factor is killed by a factor tending to 00: if u(x)B|u(x)| \le B near cc then Bxc(xc)u(x)Bxc-B|x - c| \le (x - c)u(x) \le B|x - c| near cc, and both outer functions tend to 00. That is exactly how xψ(1/x)0x\,\psi(1/x) \to 0 is proved on the companion page.

  • The sequential analogue is The squeeze theorem.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

If cc is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree

Statement

Let ARA \subseteq \mathbb{R}, let f:ARf : A \to \mathbb{R} and let cRc \in \mathbb{R} be a limit point of both A=A(,c)A^{-} = A \cap (-\infty, c) and A+=A(c,)A^{+} = A \cap (c, \infty) (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length), so that both one-sided limits at cc are well posed (The left and right limits of ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty)). Then cc is a limit point of AA, and for every LRL \in \mathbb{R}:

limxcf(x)=Llimxcf(x)=L  and  limxc+f(x)=L\lim_{x \to c} f(x) = L \quad \Longleftrightarrow \quad \lim_{x \to c^{-}} f(x) = L \ \text{ and } \ \lim_{x \to c^{+}} f(x) = L

(The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA). Consequently the limit of ff at cc exists if and only if both one-sided limits exist and are equal, and in that case

limxcf(x)  =  limxcf(x)  =  limxc+f(x).\lim_{x \to c} f(x) \;=\; \lim_{x \to c^{-}} f(x) \;=\; \lim_{x \to c^{+}} f(x) .

The hypothesis on both sides is what makes the statement an equivalence. If cc is a limit point of only one of the two sets — as 11 is for {0}[1,2]\{0\} \cup [1,2] — 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 ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty)).

Facts & Assumptions

Given: A set ARA \subseteq \mathbb{R}, a function f:ARf : A \to \mathbb{R}, a real cc that is a limit point of both A=A(,c)A^{-} = A \cap (-\infty, c) and A+=A(c,)A^{+} = A \cap (c, \infty), and a real LL (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length, The left and right limits of ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty)).

[L1]

The limit condition (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA): limxch(x)=L\lim_{x \to c} h(x) = L means that for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xx in the domain of hh with 0<xc<δ0 < |x - c| < \delta satisfies h(x)L<ε|h(x) - L| < \varepsilon.

[L2]

Limit point: cc is a limit point of SS when for every real δ>0\delta > 0 there is xSx \in S with 0<xc<δ0 < |x - c| < \delta (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L3]

Intervals: A={xA:x<c}A^{-} = \{\, x \in A : x < c \,\} and A+={xA:x>c}A^{+} = \{\, x \in A : x > c \,\} (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length).

[L4]

Absolute value and order: xc=0|x - c| = 0 exactly when x=cx = c; the order is total, so every xcx \ne c satisfies x<cx < c or x>cx > c; and 0<xc<δ0 < |x - c| < \delta is equivalent to cδ<x<cc - \delta < x < c for x<cx < c and to c<x<c+δc < x < c + \delta for x>cx > c (Basic properties of the absolute value, Ordered field). Of two positive reals the smaller is positive.

[L5]

Restriction: if BAB \subseteq A has cc as a limit point and limxcf(x)=L\lim_{x \to c} f(x) = L, then limxcfB(x)=L\lim_{x \to c} f|_B(x) = L (claim 2 of The limit at cc depends only on the restriction of ff to a punctured neighbourhood of cc, and passes to any subset of the domain having cc as a limit point).

[L6]

One-sided limits are by definition the limits of the restrictions fAf|_{A^{-}} and fA+f|_{A^{+}} at cc (The left and right limits of ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty)).

[L7]

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 fAf|_{A^{-}} and to fA+f|_{A^{+}} it makes each one-sided limit a single real, and applied to ff it does the same for the two-sided limit.

Proof

technique · direct
1.1

cc is a limit point of AA: it is one of A+A^{+} by hypothesis, and A+AA^{+} \subseteq A, so every point of A+A^{+} found in a punctured neighbourhood of cc is a point of AA there.

L2L3
1.2

For xAx \in A the condition 0<xc0 < |x - c| says exactly xcx \ne c, and then x<cx < c or x>cx > c, that is xAx \in A^{-} or xA+x \in A^{+}; moreover for xAx \in A^{-} the condition 0<xc<δ0 < |x - c| < \delta reads cδ<x<cc - \delta < x < c and for xA+x \in A^{+} it reads c<x<c+δc < x < c + \delta.

L3L4
2.1

Suppose limxcf(x)=L\lim_{x \to c} f(x) = L. Both AA^{-} and A+A^{+} are subsets of AA having cc as a limit point, so [L5] gives limxcfA(x)=L\lim_{x \to c} f|_{A^{-}}(x) = L and limxcfA+(x)=L\lim_{x \to c} f|_{A^{+}}(x) = L, which by [L6] is exactly limxcf(x)=L\lim_{x \to c^{-}} f(x) = L and limxc+f(x)=L\lim_{x \to c^{+}} f(x) = L.

step 1.1step 1.2L5L6
2.2

Suppose conversely that both one-sided limits equal LL, and let ε>0\varepsilon > 0 be an arbitrary real. By [L6] and [L1] fix reals δ1,δ2>0\delta_1, \delta_2 > 0 such that every xAx \in A^{-} with 0<xc<δ10 < |x - c| < \delta_1 and every xA+x \in A^{+} with 0<xc<δ20 < |x - c| < \delta_2 satisfies f(x)L<ε|f(x) - L| < \varepsilon; let δ\delta be the smaller of the two. Every xAx \in A with 0<xc<δ0 < |x - c| < \delta lies in AA^{-} or in A+A^{+} by step 1.2, and in either case f(x)L<ε|f(x) - L| < \varepsilon. As ε\varepsilon was arbitrary, limxcf(x)=L\lim_{x \to c} f(x) = L.

step 1.2L1L4L6choose
3.1

The displayed equivalence is steps 2.1 and 2.2. For the consequence: if the limit of ff at cc exists, say with value LL, then step 2.1 gives that both one-sided limits exist with the same value LL, so they agree; and if both one-sided limits exist and are equal, to the common value LL, then step 2.2 gives that the limit of ff at cc exists and equals LL. Each of the three symbols denotes a single real by [L7], so the three are equal.

step 2.1step 2.2L7

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 cc depends only on the restriction of ff to a punctured neighbourhood of cc, and passes to any subset of the domain having cc as a limit point; the converse has to glue two estimates, and the gluing is legitimate precisely because every point of AA other than cc lies strictly on one side of cc, 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 00, 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.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)Open item page →

Composition of limits holds under either hypothesis: ff is defined at LL with value MM, or gg avoids LL on a punctured neighbourhood of cc

Statement

Let A,BRA, B \subseteq \mathbb{R}, let g:ARg : A \to \mathbb{R} with g(A)Bg(A) \subseteq B, and let f:BRf : B \to \mathbb{R}, so that the composite fg:ARf \circ g : A \to \mathbb{R} is defined. Let cc be a limit point of AA and LL a limit point of BB (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}), and suppose the limits

limxcg(x)=LandlimyLf(y)=M\lim_{x \to c} g(x) = L \qquad \text{and} \qquad \lim_{y \to L} f(y) = M

both exist, with the stated values (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA). Suppose in addition that at least one of the following holds:

  • (i) LBL \in B and f(L)=Mf(L) = M;
  • (ii) there is a real η>0\eta > 0 with g(x)Lg(x) \ne L for every xAx \in A satisfying 0<xc<η0 < |x - c| < \eta.

Then the limit of fgf \circ g at cc exists, and

limxcf(g(x))  =  limyLf(y)  =  M.\lim_{x \to c} f\bigl(g(x)\bigr) \;=\; \lim_{y \to L} f(y) \;=\; M .

At least one extra hypothesis is necessary. With both omitted the statement is false, and FALSE: limxcf(g(x))=M\lim_{x \to c} f(g(x)) = M whenever limxcg=L\lim_{x \to c} g = L and limyLf=M\lim_{y \to L} f = M refutes it with a two-line witness in which (i) fails because f(L)Mf(L) \ne M and (ii) fails because gg is constantly equal to LL.

Why an extra hypothesis is needed at all. The inner limit controls g(x)g(x) only up to g(x)L<ρ|g(x) - L| < \rho; it does not prevent g(x)g(x) from equalling LL. But The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA says nothing about ff at the point LL, so the outer estimate is unavailable exactly at the values g(x)=Lg(x) = L. Hypothesis (i) supplies the missing value directly; hypothesis (ii) excludes those values.

Facts & Assumptions

Given: Sets A,BRA, B \subseteq \mathbb{R}, functions g:ARg : A \to \mathbb{R} with g(A)Bg(A) \subseteq B and f:BRf : B \to \mathbb{R}, a limit point cc of AA, a limit point LL of BB, and reals with limxcg(x)=L\lim_{x \to c} g(x) = L and limyLf(y)=M\lim_{y \to L} f(y) = M; and the assumption that (i) or (ii) of the statement holds (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA, Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}).

[L1]

The limit condition: limxch(x)=P\lim_{x \to c} h(x) = P means that for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xx in the domain of hh with 0<xc<δ0 < |x - c| < \delta satisfies h(x)P<ε|h(x) - P| < \varepsilon (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

[L2]

Absolute value: u0|u| \ge 0, and u=0|u| = 0 if and only if u=0u = 0 (Basic properties of the absolute value).

[L3]

Order arithmetic: of two positive reals the smaller is positive, the order being total; and trichotomy (Ordered field).

Proof

technique · cases
1.1

Let ε>0\varepsilon > 0 be an arbitrary real. By [L1] applied to ff at LL, fix a real ρ>0\rho > 0 such that every yBy \in B with 0<yL<ρ0 < |y - L| < \rho satisfies f(y)M<ε|f(y) - M| < \varepsilon; then by [L1] applied to gg at cc, with ρ\rho in the role of the tolerance, fix a real δ1>0\delta_1 > 0 such that every xAx \in A with 0<xc<δ10 < |x - c| < \delta_1 satisfies g(x)L<ρ|g(x) - L| < \rho.

L1choose
2.1

Case (i): assume LBL \in B and f(L)=Mf(L) = M, and put δ:=δ1>0\delta := \delta_1 > 0. Let xAx \in A with 0<xc<δ0 < |x - c| < \delta and set y:=g(x)y := g(x), an element of BB since g(A)Bg(A) \subseteq B; then yL<ρ|y - L| < \rho. If y=Ly = L then f(y)M=f(L)M=0=0<ε|f(y) - M| = |f(L) - M| = |0| = 0 < \varepsilon; and if yLy \ne L then 0<yL<ρ0 < |y - L| < \rho, so f(y)M<ε|f(y) - M| < \varepsilon. In both events (fg)(x)M<ε|(f \circ g)(x) - M| < \varepsilon.

step 1.1assume-case valueL1L2L3
2.2

Case (ii): assume there is a real η>0\eta > 0 with g(x)Lg(x) \ne L for every xAx \in A satisfying 0<xc<η0 < |x - c| < \eta, and let δ\delta be the smaller of δ1\delta_1 and η\eta, so δ>0\delta > 0. Let xAx \in A with 0<xc<δ0 < |x - c| < \delta and set y:=g(x)By := g(x) \in B; then yLy \ne L, so yL>0|y - L| > 0, and yL<ρ|y - L| < \rho, so 0<yL<ρ0 < |y - L| < \rho and (fg)(x)M=f(y)M<ε|(f \circ g)(x) - M| = |f(y) - M| < \varepsilon.

step 1.1assume-case avoidL1L2L3
3.1

By hypothesis at least one of (i) and (ii) holds, so in either case a real δ>0\delta > 0 has been produced with (fg)(x)M<ε|(f \circ g)(x) - M| < \varepsilon for every xAx \in A satisfying 0<xc<δ0 < |x - c| < \delta; since ε>0\varepsilon > 0 was arbitrary and cc is a limit point of AA, the limit of fgf \circ g at cc exists and equals MM.

step 2.1step 2.2L1L4cases-exhaustive

Remarks

  • The hypothesis that LL is a limit point of BB is what makes limyLf(y)\lim_{y \to L} f(y) meaningful at all (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA); it is not an extra assumption of convenience. Note that it does not follow from limxcg(x)=L\lim_{x \to c} g(x) = L: a constant gg has that limit while BB may be a set for which LL is isolated.

  • Hypothesis (i) is the continuity hypothesis in disguise. Saying LBL \in B and f(L)=M=limyLf(y)f(L) = M = \lim_{y \to L} f(y) is exactly saying that ff is continuous at LL 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 y=1/xy = 1/x are legitimate: there the inner function omits the critical value on a punctured neighbourhood for a structural reason, not by assumption on ff.

  • 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).

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

Integer part: for every real xx there is exactly one integer mm with mx<m+1m \le x < m + 1

Statement

Identify Z\mathbb{Z} with its canonical copy inside R\mathbb{R}, along the embeddings NZQR\mathbb{N} \to \mathbb{Z} \to \mathbb{Q} \to \mathbb{R} (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 xx there is exactly one integer mm with

m    x  <  m+1.m \;\le\; x \;<\; m + 1 .

It is written x\lfloor x \rfloor and called the integer part, or floor, of xx.

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 N\mathbb{N} (The well-ordering principle): the first says that xx is caught between two integers at all, the second picks the least integer above xx. Uniqueness is the discreteness of Z\mathbb{Z}: no integer lies strictly between mm and m+1m+1.

This lemma is stated once here and reused. It is what turns "the nearest integer to xx" from a picture into an object, and the companion page's oscillator ψ(x)=infnZxn\psi(x) = \inf_{n \in \mathbb{Z}} |x - n| is computed from it in one line.

Facts & Assumptions

Given: A real xx. Naturals, integers and rationals are identified with their canonical copies in R\mathbb{R} along NZQR\mathbb{N} \to \mathbb{Z} \to \mathbb{Q} \to \mathbb{R}.

[L1]

The embeddings NZQR\mathbb{N} \to \mathbb{Z} \to \mathbb{Q} \to \mathbb{R} are injective and preserve 00, 11, 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); Z\mathbb{Z} is a totally ordered commutative ring (The integers form a totally ordered ring, The integers form a commutative ring); every integer 0\ge 0 is the image of a unique natural, that map being injective and order preserving (The naturals embed in the integers); and a natural j0j \ne 0 satisfies j1j \ge 1 (Discreteness: σ(n)\sigma(n) is the immediate successor, The natural numbers N\mathbb{N} (von Neumann)).

[L2]

The image of a natural n1n \ge 1 under the composite NR\mathbb{N} \to \mathbb{R} is the canonical natural n1Rn \cdot 1_{\mathbb{R}} of Canonical naturals are positive and strictly increasing. Indeed that composite preserves 11 and addition by [L1], while n1Rn \cdot 1_{\mathbb{R}} is defined by 11R=1R1 \cdot 1_{\mathbb{R}} = 1_{\mathbb{R}} and (n+1)1R=n1R+1R(n+1) \cdot 1_{\mathbb{R}} = n \cdot 1_{\mathbb{R}} + 1_{\mathbb{R}}, so the two agree at 11 and satisfy the same recursion; induction on nn (The principle of mathematical induction) gives the identification.

[L3]

Archimedean property: for every real tt there is a natural n1n \ge 1 with t<n1Rt < n \cdot 1_{\mathbb{R}} (Every complete ordered field is Archimedean, Complete ordered field (least-upper-bound property)).

[L4]

Well-ordering principle: every nonempty subset of N\mathbb{N} has a least element (The well-ordering principle).

[L5]

Order arithmetic in R\mathbb{R}: the order is total, so the negation of t<ut < u is utu \le t; trichotomy, so t<ut < u and utu \le t cannot both hold; translation invariance (Order is preserved by adding a constant and by adding inequalities); ttt \le |t| and tt-t \le |t| (Basic properties of the absolute value); and transitivity (Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · constructive
1.1

Apply [L3] to the real x|x|: fix a natural n1n \ge 1 with x<n|x| < n. Since xxx \le |x| and xx-x \le |x|, this gives n<x<n-n < x < n.

L2L3L5choose
2.1

Put S:={kN : x<kn}S := \{\, k \in \mathbb{N} \ : \ x < k - n \,\}, where knk - n is formed in Z\mathbb{Z} and read in R\mathbb{R} through [L1]. It is a subset of N\mathbb{N}, and it is nonempty: the natural 2n2n satisfies 2nn=n>x2n - n = n > x by step 1.1, so 2nS2n \in S.

step 1.1L1L2construct
3.1

By the well-ordering principle [L4] let k0k_0 be the least element of SS.

step 2.1L4choose
4.1

The index k0k_0 is not 00: for k=0k = 0 the defining condition reads x<0n=nx < 0 - n = -n, which trichotomy excludes since n<x-n < x by step 1.1. Hence k00k_0 \ne 0, so k01k_0 \ge 1 by [L1], and k01k_0 - 1 is again a natural number.

step 1.1step 3.1L1L5
5.1

Set m:=(k01)nm := (k_0 - 1) - n, an integer. Since k01<k0k_0 - 1 < k_0 and k0k_0 is the least element of SS, the natural k01k_0 - 1 does not lie in SS, that is, x<(k01)nx < (k_0 - 1) - n fails; the order being total, m=(k01)nxm = (k_0 - 1) - n \le x.

step 3.1step 4.1L1L5construct
6.1

On the other hand k0Sk_0 \in S gives x<k0n=((k01)n)+1=m+1x < k_0 - n = \bigl((k_0 - 1) - n\bigr) + 1 = m + 1. So mx<m+1m \le x < m + 1, and existence is proved.

step 3.1step 5.1L1L5
7.1

Uniqueness: suppose an integer mm' also satisfies mx<m+1m' \le x < m' + 1 and mmm' \ne m. The order of Z\mathbb{Z} being total, one of m<mm < m' and m<mm' < m holds, and the two cases are the same with the roles of mm and mm' exchanged; so assume m<mm < m'. Then mmm' - m is an integer >0> 0, hence by [L1] the image of a natural j0j \ne 0, so j1j \ge 1 and mm1m' - m \ge 1, that is m+1mm + 1 \le m'. But then x<m+1mxx < m + 1 \le m' \le x, which trichotomy forbids. Hence m=mm' = m.

step 6.1L1L5
8.1

Therefore exactly one integer mm satisfies mx<m+1m \le x < m + 1, and we write m=xm = \lfloor x \rfloor.

step 6.1step 7.1discharge-construct

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 SS 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 x\lfloor x \rfloor is a function of xx.

  • Immediate consequences, used later. From mx<m+1m \le x < m + 1 one reads off 0xm<10 \le x - m < 1 and 0<(m+1)x10 < (m+1) - x \le 1; and x=x\lfloor x \rfloor = x exactly when xx is an integer, since an integer mm satisfies mm<m+1m \le m < m + 1 and uniqueness does the rest. The translation identity x+p=x+p\lfloor x + p \rfloor = \lfloor x \rfloor + p for an integer pp follows the same way: adding pp to mx<m+1m \le x < m+1 gives m+px+p<(m+p)+1m + p \le x + p < (m + p) + 1, and uniqueness identifies m+pm + p as the integer part of x+px + p.

  • The ceiling is not defined here and is not needed on this page; it would be the least integer x\ge x, obtained from the same set SS without the shift by one.

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

The sequence-to-ε\varepsilon direction of the Heine criterion uses countable choice for R\mathbb{R}, and where this library records that cost

What this page spends, and where

Heine criterion: limxcf(x)=L\lim_{x \to c} f(x) = L iff f(xk)Lf(x_k) \to L for every sequence in A{c}A \setminus \{c\} converging to cc is an equivalence, and its two directions do not cost the same.

  • From the ε\varepsilon-δ\delta limit to sequences — if limxcf(x)=L\lim_{x \to c} f(x) = L then f(xk)Lf(x_k) \to L for every sequence in A{c}A \setminus \{c\} tending to cc — 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 ε\varepsilon-δ\delta limit is proved there using the Axiom of Countable Choice (The Axiom of Countable Choice (ACω\mathrm{AC}_\omega)), invoked exactly once, at step 3.2. The proof assumes the limit fails, obtains for each kNk \in \mathbb{N} a nonempty set Xk={xA:0<xc<1/(k+1) and f(x)Lε0}X_k = \{\, x \in A : 0 < |x - c| < 1/(k+1) \text{ and } |f(x) - L| \ge \varepsilon_0 \,\}, and needs a single point from each of those countably many sets at once.

Why no canonical selection is available. The sets XkX_k are cut out by an inequality involving ff, about which the theorem assumes nothing. There is therefore no rule in this library that names an element of XkX_k uniformly in kk: they are subsets of R\mathbb{R}, which carries no well-ordering that ZF provides, and the sets need not be intervals, need not be closed, and need not meet Q\mathbb{Q}. That is precisely the situation The Axiom of Countable Choice (ACω\mathrm{AC}_\omega) exists for.

The same cost, recorded twice

The identical pattern occurs in the prerequisite page: in A point lies in the closure of ARA \subseteq \mathbb{R} iff some sequence in AA converges to it, so a subset of R\mathbb{R} is closed iff it is sequentially closed the right-to-left direction is choice free, while producing a sequence in AA converging to a point of A\overline{A} requires selecting one point of AA from each of the sets N1/(k+1)(x)AN_{1/(k+1)}(x) \cap A, and that item invokes ACω\mathrm{AC}_\omega 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 ε\varepsilon-δ\delta to sequences is a theorem of ZF; the converse as proved here uses ACω\mathrm{AC}_\omega; and the use is isolated to one step, so nothing else on this page inherits it.

  • Not claimed: that the converse requires ACω\mathrm{AC}_\omega. 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 RR\mathbb{R} \to \mathbb{R} 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 fgf \le g on a punctured neighbourhood of cc then limflimg\lim f \le \lim g, non-strictly), the squeeze theorem (If fghf \le g \le h near cc and ff and hh have the same limit at cc, then so does gg) and composition (Composition of limits holds under either hypothesis: ff is defined at LL with value MM, or gg avoids LL on a punctured neighbourhood of cc) are all proved directly from ε\varepsilon and δ\delta, 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 cc as soon as two sequences in A{c}A \setminus \{c\} tending to cc 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 ACω\mathrm{AC}_\omega into statements that do not need it.

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

FALSE: limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) whenever both sides exist

Statement

False claim: if ARA \subseteq \mathbb{R}, if f:ARf : A \to \mathbb{R}, if cAc \in A is a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}) and if the limit of ff at cc exists (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA), then

limxcf(x)=f(c).\lim_{x \to c} f(x) = f(c) .

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 cAc \in A. The claim is that they always agree, and that is false.

Why it is tempting. The condition f(x)L<ε|f(x) - L| < \varepsilon is imposed on points xx arbitrarily close to cc, and it feels as though x=cx = c were the limiting case of that. It is not: The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA quantifies over 0<xc<δ0 < |x - c| < \delta, and the strict inequality on the left removes x=cx = c from the quantifier entirely. Changing the value of ff at the single point cc 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 cc. This library states it as a hypothesis and never as a consequence; hypothesis (i) of Composition of limits holds under either hypothesis: ff is defined at LL with value MM, or gg avoids LL on a punctured neighbourhood of cc is exactly this condition for the outer function.

Facts & Assumptions

Given: The set A:=RA := \mathbb{R}, the point c:=0c := 0, and the function f:RRf : \mathbb{R} \to \mathbb{R} defined by f(x):=0f(x) := 0 for x0x \ne 0 and f(0):=1f(0) := 1.

[L1]

The limit condition: limxch(x)=L\lim_{x \to c} h(x) = L means that for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xx in the domain of hh with 0<xc<δ0 < |x - c| < \delta satisfies h(x)L<ε|h(x) - L| < \varepsilon (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

[L2]

Limit point: cc is a limit point of SS when every punctured neighbourhood Nε(c)N^{*}_{\varepsilon}(c) meets SS; and punctured neighbourhoods in R\mathbb{R} are never empty (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L3]

Absolute value: 0=0|0| = 0, and u0|u| \ge 0 (Basic properties of the absolute value).

[L4]

Order in R\mathbb{R}: trichotomy, so every real either equals 00 or does not, and never both; and 0<10 < 1, so 101 \ne 0 (The multiplicative identity is positive, Ordered field).

Refutation

technique · direct
1.1

The point c=0c = 0 lies in A=RA = \mathbb{R} and is a limit point of R\mathbb{R}: for every real ε>0\varepsilon > 0 the punctured neighbourhood Nε(0)N^{*}_{\varepsilon}(0) is nonempty and is contained in R\mathbb{R}, so it meets R\mathbb{R}.

L2
1.2

ff is a well-defined function on R\mathbb{R}, since by trichotomy every real either equals 00 or does not, exclusively; and the reals 00 and 11 are distinct.

L4
2.1

The limit of ff at 00 exists and equals 00: given an arbitrary real ε>0\varepsilon > 0, take δ:=1>0\delta := 1 > 0; every xRx \in \mathbb{R} with 0<x0<10 < |x - 0| < 1 has x0|x| \ne 0, hence x0x \ne 0, hence f(x)=0f(x) = 0 and f(x)0=0=0<ε|f(x) - 0| = |0| = 0 < \varepsilon.

step 1.1step 1.2L1L3L4
3.1

Yet f(0)=1f(0) = 1, and 10=limx0f(x)1 \ne 0 = \lim_{x \to 0} f(x). So at the point c=0c = 0 of the domain, which is a limit point of the domain, the limit exists and differs from the value: the claim is false.

step 1.2step 2.1L4

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 cc and taking a different value at cc 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 limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) — which is what continuity at cc 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 f(c)f(c) is invisible to the limit, substituting an inner function that takes the value cc is not licensed by the limits alone; that is the content of FALSE: limxcf(g(x))=M\lim_{x \to c} f(g(x)) = M whenever limxcg=L\lim_{x \to c} g = L and limyLf=M\lim_{y \to L} f = M, whose witness is built from this one.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

FALSE: limxcf(g(x))=M\lim_{x \to c} f(g(x)) = M whenever limxcg=L\lim_{x \to c} g = L and limyLf=M\lim_{y \to L} f = M

Statement

False claim: let A,BRA, B \subseteq \mathbb{R}, let g:ARg : A \to \mathbb{R} with g(A)Bg(A) \subseteq B and f:BRf : B \to \mathbb{R}, let cc be a limit point of AA and LL a limit point of BB. If

limxcg(x)=LandlimyLf(y)=M,\lim_{x \to c} g(x) = L \qquad \text{and} \qquad \lim_{y \to L} f(y) = M ,

then the limit of fgf \circ g at cc exists and limxcf(g(x))=M\lim_{x \to c} f\bigl(g(x)\bigr) = M (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

This is the statement of Composition of limits holds under either hypothesis: ff is defined at LL with value MM, or gg avoids LL on a punctured neighbourhood of cc with both of its extra hypotheses removed, and it is false. It is refuted below by a pair in which gg is constant and ff has a removable defect at the value of that constant.

Where the naive argument breaks. The inner limit gives g(x)L<ρ|g(x) - L| < \rho for xx near cc; the outer limit gives f(y)M<ε|f(y) - M| < \varepsilon for yBy \in B with 0<yL<ρ0 < |y - L| < \rho. To combine them at y=g(x)y = g(x) one needs g(x)L>0|g(x) - L| > 0, and nothing in the hypotheses supplies that. Where g(x)=Lg(x) = L, the only information available about ff is its value f(L)f(L), and The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA says nothing whatever about that value (FALSE: limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) whenever both sides exist). The two hypotheses of Composition of limits holds under either hypothesis: ff is defined at LL with value MM, or gg avoids LL on a punctured neighbourhood of cc are exactly the two ways of closing that gap.

Facts & Assumptions

Given: The sets A:=RA := \mathbb{R} and B:=RB := \mathbb{R}; the point c:=0c := 0; the function f:RRf : \mathbb{R} \to \mathbb{R} of FALSE: limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) whenever both sides exist, namely f(y):=0f(y) := 0 for y0y \ne 0 and f(0):=1f(0) := 1; and the constant function g:RRg : \mathbb{R} \to \mathbb{R}, g(x):=0g(x) := 0 for every xx.

[L1]

The limit condition (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA): limxch(x)=P\lim_{x \to c} h(x) = P means that for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xx in the domain of hh with 0<xc<δ0 < |x - c| < \delta satisfies h(x)P<ε|h(x) - P| < \varepsilon.

[L3]

Absolute value: 0=0|0| = 0 (Basic properties of the absolute value).

[L4]

Order in R\mathbb{R}: trichotomy, and 0<10 < 1, so 101 \ne 0 (The multiplicative identity is positive, Ordered field).

[L5]

The function ff above satisfies f(0)=1f(0) = 1 and has limit 00 at 00: for every real ε>0\varepsilon > 0 the radius δ=1\delta = 1 works, since 0<y0<10 < |y - 0| < 1 forces y0y \ne 0 and then f(y)0=0<ε|f(y) - 0| = 0 < \varepsilon; this is the computation carried out in FALSE: limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) whenever both sides exist.

Refutation

technique · direct
1.1

The point 00 is a limit point of R\mathbb{R}, and g(R)={0}R=Bg(\mathbb{R}) = \{0\} \subseteq \mathbb{R} = B, so fgf \circ g is a function on R\mathbb{R}.

L2
1.2

By [L5], limy0f(y)=0\lim_{y \to 0} f(y) = 0; so the outer hypothesis holds with L=0L = 0 and M=0M = 0.

L5
1.3

The reals 00 and 11 are distinct.

L4
2.1

The inner hypothesis holds with L=0L = 0: for the constant function gg and any real ε>0\varepsilon > 0, every δ>0\delta > 0 works, since g(x)0=0=0<ε|g(x) - 0| = |0| = 0 < \varepsilon for every xx. So limx0g(x)=0\lim_{x \to 0} g(x) = 0.

step 1.1L1L3
3.1

But fgf \circ g is the constant function 11: for every xRx \in \mathbb{R}, g(x)=0g(x) = 0 and hence f(g(x))=f(0)=1f(g(x)) = f(0) = 1. Therefore, by the same computation as in step 2.1, the limit of fgf \circ g at 00 exists and equals 11.

step 2.1L1L3L5
3.2

Both extra hypotheses of Composition of limits holds under either hypothesis: ff is defined at LL with value MM, or gg avoids LL on a punctured neighbourhood of cc fail for this pair: hypothesis (i) fails because L=0L = 0 lies in B=RB = \mathbb{R} while f(L)=f(0)=10=Mf(L) = f(0) = 1 \ne 0 = M; and hypothesis (ii) fails because g(x)=0=Lg(x) = 0 = L for every xx, so no punctured neighbourhood of 00 avoids the value LL.

step 2.1L5L6
4.1

So limx0g(x)=0=L\lim_{x \to 0} g(x) = 0 = L and limy0f(y)=0=M\lim_{y \to 0} f(y) = 0 = M, while limx0f(g(x))=10=M\lim_{x \to 0} f(g(x)) = 1 \ne 0 = M: the claim is false, and step 3.2 identifies exactly which hypotheses of the true theorem are missing.

step 1.2step 1.3step 3.1step 3.2

Remarks

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

FALSE: a function has at most one limit at every point of its domain, isolated points included

Statement

False claim: for every ARA \subseteq \mathbb{R}, every f:ARf : A \to \mathbb{R} and every cAc \in A, at most one real LL satisfies

(ε>0) (δ>0) (xA) [ 0<xc<δ  f(x)L<ε ].()(\forall \varepsilon > 0)\ (\exists \delta > 0)\ (\forall x \in A)\ \bigl[\ 0 < |x - c| < \delta \ \Longrightarrow\ |f(x) - L| < \varepsilon\ \bigr] . \qquad (\ast)

Read the claim carefully: it is about the raw formula ()(\ast), extended to an arbitrary point cc of the domain. It is not a claim about The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA. That definition imposes ()(\ast) only when cc is a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}), and there at most one LL 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 AA the symbol limxcf(x)\lim_{x \to c} f(x) is undefined in this library, and the refutation below is the reason. If cAc \in A is not a limit point of AA then some punctured neighbourhood of cc misses AA entirely (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}); the implication inside ()(\ast) then has no instances at all for that δ\delta, so it holds vacuously, and it holds for every real LL at once. A formula satisfied by every real determines nothing, so no notation is introduced for it.

Facts & Assumptions

Given: The set A:={0}[1,2]A := \{0\} \cup [1,2] (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length), the constant function f:ARf : A \to \mathbb{R} with f(x):=0f(x) := 0 for every xAx \in A, and the point c:=0Ac := 0 \in A.

[L1]

The ε\varepsilon-δ\delta formula ()(\ast) above, and the fact that The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA imposes it only at a limit point of the domain.

[L2]

Limit point and isolated point: cc is a limit point of SS when Nε(c)SN^{*}_{\varepsilon}(c) \cap S \ne \varnothing for every real ε>0\varepsilon > 0, and cSc \in S is an isolated point of SS when Nε(c)S={c}N_{\varepsilon}(c) \cap S = \{c\} for some real ε>0\varepsilon > 0; for cSc \in S these are exact opposites (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L3]

Neighbourhoods: N1(0)={y:y<1}N_{1}(0) = \{\, y : |y| < 1 \,\} and N1(0)={y:0<y<1}N^{*}_{1}(0) = \{\, y : 0 < |y| < 1 \,\} (The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L4]

Absolute value and order: u0|u| \ge 0; u=0|u| = 0 exactly when u=0u = 0; u=u|u| = u for u0u \ge 0; the order is total and trichotomy holds; and 0<10 < 1, so 010 \ne 1 (Basic properties of the absolute value, The multiplicative identity is positive, Ordered field).

[L5]

Intervals: [1,2]={y:1y2}[1,2] = \{\, y : 1 \le y \le 2 \,\} (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length).

Refutation

technique · direct
1.1

The point 00 lies in AA, and N1(0)A={0}N_{1}(0) \cap A = \{0\}: an element of AA is either 00, which satisfies 0=0<1|0| = 0 < 1, or an element of [1,2][1,2], which satisfies y=y1|y| = y \ge 1 and so is not in N1(0)N_1(0). Hence 00 is an isolated point of AA and not a limit point of AA.

L2L3L4L5
1.2

The reals 00 and 11 are distinct.

L4
2.1

Take δ:=1\delta := 1. No xAx \in A satisfies 0<x0<10 < |x - 0| < 1: such an xx would lie in N1(0)AN^{*}_{1}(0) \cap A, which is contained in N1(0)A={0}N_1(0) \cap A = \{0\} and excludes 00, hence is empty. So for every real LL and every real ε>0\varepsilon > 0 the choice δ=1\delta = 1 makes the implication in ()(\ast) vacuously true, and every real LL satisfies ()(\ast) at c=0c = 0.

step 1.1L1L3L4
3.1

In particular L=0L = 0 and L=1L = 1 both satisfy ()(\ast) at c=0c = 0, and they are distinct: more than one real satisfies the formula, so the claim is false.

step 1.2step 2.1L4

Remarks

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

FALSE: f<gf < g near cc implies limf<limg\lim f < \lim g

Statement

False claim: let ARA \subseteq \mathbb{R}, let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}), let f,g:ARf, g : A \to \mathbb{R} have limits at cc (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA), and suppose there is a real η>0\eta > 0 with

f(x)<g(x)for every xA with 0<xc<η.f(x) < g(x) \qquad \text{for every } x \in A \text{ with } 0 < |x - c| < \eta .

Then limxcf(x)<limxcg(x)\lim_{x \to c} f(x) < \lim_{x \to c} g(x).

What is true is the non-strict version, If fgf \le g on a punctured neighbourhood of cc then limflimg\lim f \le \lim g, non-strictly: the hypothesis fgf \le g near cc gives limflimg\lim f \le \lim g, 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 g(x)f(x)>0g(x) - f(x) > 0 for every xx near cc, with no lower bound on that positive quantity. The limit only sees the limit of gfg - f, and a function that is positive everywhere may have limit 00. What does survive is the uniform version: if g(x)f(x)κg(x) - f(x) \ge \kappa near cc for a fixed real κ>0\kappa > 0, then limglimfκ>0\lim g - \lim f \ge \kappa > 0, by applying If fgf \le g on a punctured neighbourhood of cc then limflimg\lim f \le \lim g, non-strictly to f+κf + \kappa and gg.

Facts & Assumptions

Given: The set A:=RA := \mathbb{R}, the point c:=0c := 0, the constant function f:RRf : \mathbb{R} \to \mathbb{R} with f(x):=0f(x) := 0 for every xx, and the function g:RRg : \mathbb{R} \to \mathbb{R} with g(x):=xg(x) := |x|.

[L1]

The limit condition (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA): limxch(x)=P\lim_{x \to c} h(x) = P means that for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xx in the domain of hh with 0<xc<δ0 < |x - c| < \delta satisfies h(x)P<ε|h(x) - P| < \varepsilon.

[L3]

Absolute value: u0|u| \ge 0; u=0|u| = 0 exactly when u=0u = 0; and u=u|u| = u for u0u \ge 0, so x0=x\bigl| |x| - 0 \bigr| = |x| (Basic properties of the absolute value).

[L4]

Order in R\mathbb{R}: trichotomy, so u0|u| \ge 0 together with u0|u| \ne 0 gives u>0|u| > 0, and t<tt < t is impossible (Ordered field).

Refutation

technique · direct
1.1

The point 00 is a limit point of R\mathbb{R}.

L2
1.2

The strict hypothesis holds with η:=1\eta := 1: every xRx \in \mathbb{R} with 0<x0<10 < |x - 0| < 1 has x0|x| \ne 0, hence x>0=f(x)|x| > 0 = f(x), that is f(x)<g(x)f(x) < g(x).

L3L4
2.1

Both limits exist and are equal to 00. For ff: f(x)0=0<ε|f(x) - 0| = 0 < \varepsilon for every xx and every real ε>0\varepsilon > 0, any δ\delta serving. For gg: given a real ε>0\varepsilon > 0 take δ:=ε\delta := \varepsilon; every xx with 0<x0<δ0 < |x - 0| < \delta satisfies x0=x<ε\bigl| |x| - 0 \bigr| = |x| < \varepsilon.

step 1.1L1L3
3.1

So f(x)<g(x)f(x) < g(x) throughout a punctured neighbourhood of 00 while limx0f(x)=0=limx0g(x)\lim_{x \to 0} f(x) = 0 = \lim_{x \to 0} g(x); the asserted strict inequality 0<00 < 0 is impossible by trichotomy, so the claim is false.

step 1.2step 2.1L4

Remarks

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

FALSE: a function with a limit at cc is bounded on its whole domain

Statement

False claim: let ARA \subseteq \mathbb{R}, let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}) and let f:ARf : A \to \mathbb{R} have a limit at cc (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA). Then ff is bounded on AA, that is, the image f(A)f(A) is a bounded subset of R\mathbb{R} (Lower bound, bounded below, bounded set).

What is true is the local statement, If ff has a finite limit at cc then ff is bounded on some punctured neighbourhood of cc: there is a radius δ>0\delta > 0 such that ff is bounded on ANδ(c)A \cap N^{*}_{\delta}(c). The radius is produced by the limit condition at the single tolerance ε=1\varepsilon = 1, and it carries no information whatever about the values of ff far from cc, which the limit condition never constrains.

The witness below is f(x)=1/xf(x) = 1/x on (0,)(0, \infty) at the point c=1c = 1: the limit there is 11, and ff is bounded near 11, while on the whole domain ff takes values above every real.

Facts & Assumptions

Given: The set A:=(0,)A := (0, \infty) (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length), the point c:=1c := 1, and the function f:ARf : A \to \mathbb{R} with f(x):=1/x=x1f(x) := 1/x = x^{-1}.

[L1]

The limit condition (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA): limxch(x)=P\lim_{x \to c} h(x) = P means that for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xx in the domain of hh with 0<xc<δ0 < |x - c| < \delta satisfies h(x)P<ε|h(x) - P| < \varepsilon.

[L3]

Absolute value: u0|u| \ge 0; u=u|u| = u for u0u \ge 0; uv=uv|uv| = |u|\,|v|; u=u|-u| = |u|; and for t>0t > 0, u<t|u| < t is equivalent to t<u<t-t < u < t (Basic properties of the absolute value).

[L4]

Inverses and order: a>0a > 0 gives a1>0a^{-1} > 0, and 0<a<b0 < a < b gives 0<b1<a10 < b^{-1} < a^{-1} (Inverses of positives are positive, and reciprocation reverses order); (a1)1=a(a^{-1})^{-1} = a for a0a \ne 0, inverses being unique (Field); and for t>0t > 0, u<vu < v is equivalent to ut<vtut < vt (Sign rules for products and monotonicity of multiplication).

[L5]

Order arithmetic: 0<10 < 1, hence 2>02 > 0 and 1/2>01/2 > 0 with 11/2=1/21 - 1/2 = 1/2 (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).

[L6]

Archimedean property: for every real MM there is a natural n1n \ge 1 with M<n1RM < n \cdot 1_{\mathbb{R}}, and the canonical naturals satisfy n1R>0n \cdot 1_{\mathbb{R}} > 0 (Every complete ordered field is Archimedean, Canonical naturals are positive and strictly increasing, Complete ordered field (least-upper-bound property)).

[L7]

Bounded set: SRS \subseteq \mathbb{R} 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

technique · direct
1.1

The point 11 lies in A=(0,)A = (0,\infty) and is a limit point of AA: given a real ε>0\varepsilon > 0, let ρ\rho be the smaller of ε\varepsilon and 11, so ρ>0\rho > 0; then 1+ρ/2>1>01 + \rho/2 > 1 > 0 lies in AA and satisfies 0<(1+ρ/2)1=ρ/2<ε0 < |(1 + \rho/2) - 1| = \rho/2 < \varepsilon.

L2L3L5
1.2

ff is well defined on AA: every xAx \in A has x>0x > 0, hence x0x \ne 0 and x1x^{-1} exists, with x1>0x^{-1} > 0.

L4L7
2.1

The limit of ff at 11 exists and equals 11. Let ε>0\varepsilon > 0 be an arbitrary real and let δ\delta be the smaller of 1/21/2 and ε/2\varepsilon/2, so δ>0\delta > 0. For xAx \in A with 0<x1<δ0 < |x - 1| < \delta we get x>11/2=1/2>0x > 1 - 1/2 = 1/2 > 0, hence 0<1/x<20 < 1/x < 2 by [L4]; and 1/x1=(1x)/x=x1(1/x)<δ2ε|1/x - 1| = |(1 - x)/x| = |x - 1| \cdot (1/x) < \delta \cdot 2 \le \varepsilon.

step 1.1step 1.2L1L3L4L5
2.2

The image f(A)f(A) has no upper bound. Let MM be an arbitrary real; by [L6] fix a natural n1n \ge 1 with M<n1RM < n \cdot 1_{\mathbb{R}}, and note n1R>0n \cdot 1_{\mathbb{R}} > 0. Then x:=(n1R)1x := (n \cdot 1_{\mathbb{R}})^{-1} satisfies x>0x > 0, so xAx \in A, and f(x)=x1=n1R>Mf(x) = x^{-1} = n \cdot 1_{\mathbb{R}} > M. So no real bounds f(A)f(A) above, and f(A)f(A) is not bounded.

step 1.2L4L6L7
3.1

So ff has a limit at the limit point c=1c = 1 of its domain and is unbounded on that domain: the claim is false, while If ff has a finite limit at cc then ff is bounded on some punctured neighbourhood of cc remains true and gives boundedness on AN1/2(1)A \cap N^{*}_{1/2}(1), where indeed 0<f(x)<20 < f(x) < 2 by step 2.1.

step 2.1step 2.2L7

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 cc 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 AA outside a punctured neighbourhood of cc can be infinite and can carry arbitrary values.

  • A bounded version does hold with an extra hypothesis: if AA is itself contained in a punctured neighbourhood of cc 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