CounterexampleConstruction: AI-adaptedVerification: 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.

The indicator of $Q$ has a limit at no point of $R$

Statement refuted

Write $Q$ for the canonical copy of the rationals inside $R$ (The rationals embed densely in the reals), $X : = R ∖ Q$ for the irrationals, and let

$1_{Q} : R \to R, 1_{Q} (x) : = {\begin{cases} 1 & x \in Q, \\ 0 & x \in X . \end{cases}$

Refuted claim: there is a point $c \in R$ at which $1_{Q}$ has a limit (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

The refutation fixes an arbitrary real $c$ and produces two sequences tending to $c$ , one of rationals and one of irrationals, both avoiding $c$ ; the image sequences are constantly $1$ and constantly $0$ , and A function has no limit at $c$ as soon as two sequences in $A ∖ {c}$ tending to $c$ give different limits of the values applies. Since $c$ was arbitrary, the function has a limit nowhere.

Where the choice principle enters, and where it does not. Producing the two sequences is a use of A point lies in the closure of $A \subseteq R$ iff some sequence in $A$ converges to it, so a subset of $R$ is closed iff it is sequentially closed, whose left-to-right direction spends countable choice, and that cost is inherited here and recorded by that item. The criterion applied afterwards is the choice-free one (A function has no limit at $c$ as soon as two sequences in $A ∖ {c}$ tending to $c$ give different limits of the values).

Facts & Assumptions

Given: The canonical copy $Q \subseteq R$ of the rationals, the irrationals $X = R ∖ Q$ , the function $1_{Q}$ above, and an arbitrary real $c$ .

[L1]

Density: $Q$ and $X$ are both dense in $R$ , that is, each has closure $R$ (Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable); and the closure of a set $S$ is exactly the set of points every neighbourhood of which meets $S$ (The closure equals the set together with its limit points, equals the set of points every neighbourhood of which meets it, and is the smallest closed superset; a set is closed iff it contains its limit points, Interior, closure, boundary and exterior of a subset of $R$ , Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L2]

Sequential characterisation of the closure: $x$ lies in the closure of $S$ if and only if there is a sequence with all terms in $S$ converging to $x$ (A point lies in the closure of $A \subseteq R$ iff some sequence in $A$ converges to it, so a subset of $R$ is closed iff it is sequentially closed, Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals). The direction used below, from the closure to a sequence, is the one that spends countable choice, as that item records.

[L3]

Neighbourhoods: $N_{ρ} (u) = {y : ∣ y - u ∣ < ρ}$ for real $ρ > 0$ , so $N_{ε / 2} (c + ε / 2) = {y : c < y < c + ε}$ (The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

[L4]

Nonexistence criterion: if two sequences with all terms in $A ∖ {c}$ converge to $c$ while the image sequences converge to distinct reals, then the function has no limit at $c$ (A function has no limit at $c$ as soon as two sequences in $A ∖ {c}$ tending to $c$ give different limits of the values).

[L5]

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

[L6]

A constant sequence converges to its value (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L7]

Absolute value and order: $∣ u ∣ \geq 0$ and $∣ u ∣ = u$ for $u \geq 0$ (Basic properties of the absolute value); $0 < 1$ , so $2 > 0$ , $ε / 2 > 0$ and $ε / 2 < ε$ for $ε > 0$ ; trichotomy and totality (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Inverses of positives are positive, and reciprocation reverses order, Ordered field).

Counterexample

technique · direct

1.1

Let $c \in R$ be arbitrary. Then $c$ is a limit point of $R$ , the domain of $1_{Q}$ , so the question of a limit at $c$ is well posed.

1.2

Let $S$ be either $Q$ or $X$ , and let $ε > 0$ be an arbitrary real. Applying [L1] at the real $c + ε / 2$ with the radius $ε / 2 > 0$ , the neighbourhood $N_{ε / 2} (c + ε / 2)$ meets $S$ ; and by [L3] every $y$ in that neighbourhood satisfies $c < y < c + ε$ , hence $y \neq c$ and $0 < ∣ y - c ∣ < ε$ . So every neighbourhood of $c$ meets $S ∖ {c}$ .

L1L3L7

2.1

By [L1] again, step 1.2 says exactly that $c$ lies in the closure of $Q ∖ {c}$ and in the closure of $X ∖ {c}$ . Hence [L2] supplies a sequence $(q_{k})$ with all terms in $Q ∖ {c}$ converging to $c$ , and a sequence $(u_{k})$ with all terms in $X ∖ {c}$ converging to $c$ .

step 1.2L1L2choose

3.1

Every term of $(q_{k})$ lies in $Q$ , so $1_{Q} (q_{k}) = 1$ for every $k$ and the image sequence is the constant sequence $1$ , converging to $1$ ; every term of $(u_{k})$ lies in $X$ , so $1_{Q} (u_{k}) = 0$ for every $k$ and that image sequence converges to $0$ . The reals $1$ and $0$ are distinct.

step 2.1L6L7

4.1

Both sequences have all their terms in $R ∖ {c}$ and converge to $c$ , while their image sequences converge to distinct reals; by [L4] the function $1_{Q}$ has no limit at $c$ . Since $c \in R$ was arbitrary, it has a limit at no point of $R$ .

step 1.1step 2.1step 3.1L4∎

Remarks

Why the sets are punctured before the sequences are drawn. A function has no limit at $c$ as soon as two sequences in $A ∖ {c}$ tending to $c$ give different limits of the values requires all terms to lie in $A ∖ {c}$ , since a sequence allowed to take the value $c$ would report on $1_{Q} (c)$ , which the limit ignores (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ). Step 1.2 therefore verifies density of $Q ∖ {c}$ and of $X ∖ {c}$ directly, by placing the auxiliary neighbourhood strictly to the right of $c$ .
The two densities are not proved the same way. $Q$ is dense because it is built to approximate; $X$ is dense because a countable set cannot exhaust an interval. Both are claims 1 and 2 of Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable, and this item uses them only through the neighbourhood formulation of [L1].
The failure is as total as possible. Not merely does the limit fail at some points: it fails at every point of $R$ , while the function is bounded throughout, taking only the values $0$ and $1$ . Multiplying by $x$ leaves exactly one point where a limit survives, which is $x \cdot 1_{Q} (x)$ has a limit at $0$ and at no other point.

Depends on

Used by

x · 1_ℚ(x) has a limit at 0 and at no other point Example

Dependency tree · two levels

48 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

Dirichlet function (Wikipedia) (standard reference, not scraped)
Limit of a function (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)

The indicator of QQ has a limit at no point of RR