CounterexampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)

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.

With $g \equiv 0$ and $f$ equal to $0$ off the origin and $1$ at it, $\lim g = 0$ and $\lim_{y \to 0} f = 0$ while $f \circ g \equiv 1$

Statement refuted

Refuted claim: if $\lim_{x \to c} g(x) = L$ and $\lim_{y \to L} f(y) = M$ then the limit of $f \circ g$ at $c$ exists and equals $M$ — the false statement FALSE: $\lim_{x \to c} f(g(x)) = M$ whenever $\lim_{x \to c} g = L$ and $\lim_{y \to L} f = M$ .

Take $A = B = \mathbb{R}$ , $c = 0$ , the constant function $g \equiv 0$ , and the function $f$ of The function equal to $0$ off the origin and to $1$ at the origin has limit $0 \ne 1$ there, equal to $0$ off the origin and to $1$ at it. Then $L = 0$ , $M = 0$ , and $f \circ g$ is the constant function $1$ , so the limit of $f \circ g$ at $0$ exists and equals $1 \ne 0 = M$ .

What this item adds to the false statement. It carries the comparison through: it identifies which of the two hypotheses of Composition of limits holds under either hypothesis: $f$ is defined at $L$ with value $M$ , or $g$ avoids $L$ on a punctured neighbourhood of $c$ fails here — both do — and it shows that replacing the inner function by the identity, which satisfies hypothesis (ii), restores the conclusion with the same outer function. So neither the outer function nor the composition operation is at fault; the failure is precisely that the inner function takes the critical value.

Facts & Assumptions

Given: The function $f : \mathbb{R} \to \mathbb{R}$ of The function equal to $0$ off the origin and to $1$ at the origin has limit $0 \ne 1$ there, with $f(y) = 0$ for $y \ne 0$ and $f(0) = 1$ ; the constant function $g : \mathbb{R} \to \mathbb{R}$ , $g(x) = 0$ ; the identity function $\iota : \mathbb{R} \to \mathbb{R}$ , $\iota(x) = x$ ; and the point $c := 0$ .

[L1]

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

[L2]

Every real is a limit point of $\mathbb{R}$ , punctured neighbourhoods being never empty (Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$ , The $\varepsilon$ -neighbourhood and the punctured $\varepsilon$ -neighbourhood of a point of $\mathbb{R}$ ).

[L3]

The witness function: $f(0) = 1$ by its definition, and the limit of $f$ at $0$ exists and equals $0$ , as verified in The function equal to $0$ off the origin and to $1$ at the origin has limit $0 \ne 1$ there.

[L4]

Absolute value: $|0| = 0$ ; $|u| = 0$ exactly when $u = 0$ (Basic properties of the absolute value).

[L5]

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

[L6]

Composition of limits, and its two extra hypotheses: (i) $L \in B$ and $f(L) = M$ ; (ii) some real $\eta > 0$ has $g(x) \ne L$ for every $x \in A$ with $0 < |x - c| < \eta$ (Composition of limits holds under either hypothesis: $f$ is defined at $L$ with value $M$ , or $g$ avoids $L$ on a punctured neighbourhood of $c$ ).

Counterexample

technique · direct

1.1

By [L3] the limit of $f$ at $0$ exists and equals $0$ , and $f(0) = 1$ ; so the outer hypothesis of the refuted claim holds with $L = 0$ and $M = 0$ .

1.2

$0$ is a limit point of $\mathbb{R}$ , and $g(\mathbb{R}) = \{0\} \subseteq \mathbb{R}$ and $\iota(\mathbb{R}) = \mathbb{R}$ , so both $f \circ g$ and $f \circ \iota$ are functions on $\mathbb{R}$ .

1.3

The reals $0$ and $1$ are distinct.

2.1

The inner hypothesis holds for $g$ with $L = 0$ : for every real $\varepsilon > 0$ every $\delta > 0$ serves, since $|g(x) - 0| = |0| = 0 < \varepsilon$ for every $x$ . So the limit of $g$ at $0$ exists and equals $0$ .

step 1.2L1L4

2.2

It holds for $\iota$ as well: given a real $\varepsilon > 0$ take $\delta := \varepsilon$ ; then $0 < |x - 0| < \delta$ gives $|\iota(x) - 0| = |x| < \varepsilon$ . So the limit of $\iota$ at $0$ exists and equals $0$ .

step 1.2L1

3.1

$f \circ g$ is the constant function $1$ : for every $x \in \mathbb{R}$ , $g(x) = 0$ and hence $f(g(x)) = f(0) = 1$ . By the computation of step 2.1, applied to the constant $1$ in place of the constant $0$ , the limit of $f \circ g$ at $0$ exists and equals $1$ .

step 1.1step 2.1L1L4

3.2

$f \circ \iota = f$ , since $f(\iota(x)) = f(x)$ for every $x$ ; so by [L3] the limit of $f \circ \iota$ at $0$ exists and equals $0 = M$ .

step 1.1step 2.2L3

4.1

Hence $\lim_{x \to 0} g(x) = 0 = L$ and $\lim_{y \to 0} f(y) = 0 = M$ , while $\lim_{x \to 0} f(g(x)) = 1 \ne 0 = M$ : the refuted claim is false.

step 1.3step 3.1L5

4.2

Both extra hypotheses of Composition of limits holds under either hypothesis: $f$ is defined at $L$ with value $M$ , or $g$ avoids $L$ on a punctured neighbourhood of $c$ fail for the pair $(f, g)$ : hypothesis (i) fails because $L = 0$ lies in $B = \mathbb{R}$ while $f(L) = f(0) = 1 \ne 0 = M$ , and hypothesis (ii) fails because $g(x) = 0 = L$ for every $x$ , so no punctured neighbourhood of $0$ avoids the value $L$ . For the pair $(f, \iota)$ , hypothesis (ii) does hold with $\eta := 1$ , since $\iota(x) = x \ne 0$ whenever $0 < |x - 0| < 1$ ; and step 3.2 confirms the conclusion of the theorem there.

step 1.1step 3.1step 3.2L6

5.1

So the two safeguards in the true theorem cannot both be omitted, and the obstruction is located exactly at the values of the inner function that equal $L$ .

step 4.1step 4.2∎

Remarks

The same outer function serves both roles. With $g$ the composition fails, with $\iota$ it succeeds, and $f$ is unchanged. So the failure cannot be attributed to any pathology of $f$ beyond the one recorded in The function equal to $0$ off the origin and to $1$ at the origin has limit $0 \ne 1$ there: that its value at $0$ differs from its limit at $0$ .
Constancy of $g$ is not the issue either. What matters is that $g$ takes the value $L$ on every punctured neighbourhood of $c$ . Any inner function doing that, constant or not, produces the same failure by the same argument, since the outer estimate is unavailable at those arguments.
The practical rule. When substituting $y = g(x)$ inside a limit, check one of the two hypotheses of Composition of limits holds under either hypothesis: $f$ is defined at $L$ with value $M$ , or $g$ avoids $L$ on a punctured neighbourhood of $c$ : either the outer function is defined at $L$ with the right value there, or the inner function avoids $L$ near $c$ . Substitutions such as $y = 1/x$ satisfy the second for structural reasons; substitutions into a function known only through its limit satisfy neither in general.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

Sources

J. Lebl, Basic Analysis I, §3.1: Limits of functions (standard reference, not scraped)
Limit of a function (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §9.3 (standard reference, not scraped)

With g≡0g \equiv 0g≡0 and fff equal to 000 off the origin and 111 at it, lim⁡g=0\lim g = 0limg=0 and lim⁡y→0f=0\lim_{y \to 0} f = 0limy→0​f=0 while f∘g≡1f \circ g \equiv 1f∘g≡1