CorollaryStatement: AI-adaptedProof: AI-generatedprecheck 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.

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

Statement

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

There are sequences $(x_{k})$ and $(y_{k})$ with all terms in $A ∖ {c}$ , both converging to $c$ , and reals $P \neq Q$ with $f (x_{k}) \to P$ and $f (y_{k}) \to Q$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).
There is a sequence $(x_{k})$ with all terms in $A ∖ {c}$ , converging to $c$ , for which $(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: $\lim_{x \to c} f (x) = L$ iff $f (x_{k}) \to L$ for every sequence in $A ∖ {c}$ converging to $c$ , which is a theorem of ZF; no sequence is constructed here, both being supplied by the hypothesis. So this corollary, the workhorse for showing that a limit fails to exist, costs no choice principle at all.

Facts & Assumptions

Given: A set $A \subseteq R$ , a function $f : A \to R$ and a limit point $c$ of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

[L1]

Heine criterion, the direction from the $ε$ - $δ$ limit to sequences: if $\lim_{x \to c} f (x) = L$ then $f (z_{k}) \to L$ for every sequence $(z_{k})$ with all terms in $A ∖ {c}$ converging to $c$ (Heine criterion: $\lim_{x \to c} f (x) = L$ iff $f (x_{k}) \to L$ for every sequence in $A ∖ {c}$ converging to $c$ ). 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$ $f$ has no limit at $c$ "; we prove the contrapositive of each, namely that if some $L \in R$ satisfies $\lim_{x \to c} f (x) = L$ then neither hypothesis can hold.

contrapositive-reduce

1.2

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

assume-hyp

2.1

Let $(z_{k})$ be an arbitrary sequence with all terms in $A ∖ {c}$ converging to $c$ . By [L1], $(f (z_{k}))$ converges, with limit $L$ .

step 1.2L1

3.1

Under hypothesis 1 this applies to $(x_{k})$ and to $(y_{k})$ : $f (x_{k}) \to P$ and $f (x_{k}) \to L$ give $P = L$ by [L2], and likewise $Q = L$ , so $P = Q$ ; hypothesis 1, which asserts $P \neq Q$ , therefore fails.

step 2.1L2

3.2

Under hypothesis 2 it applies to $(x_{k})$ and gives that $(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 $f$ at $c$ excludes both hypotheses; contrapositively, either hypothesis excludes the existence of a limit of $f$ at $c$ .

step 3.1step 3.2discharge-contrapositive∎

Remarks

This is the standard way a limit is shown not to exist, and the reason is that the direct route would have to refute a statement beginning "there exists $L$ ": one would have to argue about every real $L$ at once. Two sequences reduce that to a single computation, as on the companion page for $ψ (1 / x)$ at $0$ and for the indicator of $Q$ at every point.
The hypothesis "all terms in $A ∖ {c}$ " is not decorative. A sequence allowed to take the value $c$ carries information about $f (c)$ , which The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ deliberately ignores; the constant sequence $z_{k} = c$ would then refute every limit at once.
What the corollary does not say. It gives a sufficient condition for the limit not to exist, not a necessary one in any weaker form: the converse statement, that a limit exists as soon as all such image sequences converge to one value, is the other direction of Heine criterion: $\lim_{x \to c} f (x) = L$ iff $f (x_{k}) \to L$ for every sequence in $A ∖ {c}$ converging to $c$ and is exactly the direction that spends countable choice (The sequence-to- $ε$ direction of the Heine criterion uses countable choice for $R$ , and where this library records that cost).

Depends on

Used by

x sin(1/x) extended by zero is continuous but not differentiable at zero Corollary
The indicator of ℚ has a limit at no point of ℝ Counterexample
ψ(1/x) has no limit at 0: two sequences tending to 0 give values constantly 0 and constantly 1/2 Counterexample
x · 1_ℚ(x) has a limit at 0 and at no other point Example

Dependency tree · two levels

28 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on 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)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 4 (Cor. to Thm 4.2) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)

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