Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

If 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.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 29 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources