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

$x \cdot 1_{\mathbb{Q}}(x)$ has a limit at $0$ and at no other point

Example

With $\mathbf{1}_{\mathbb{Q}}$ as in The indicator of $\mathbb{Q}$ has a limit at no point of $\mathbb{R}$ , let

$d : \mathbb{R} \to \mathbb{R}, \qquad d(x) := x \cdot \mathbf{1}_{\mathbb{Q}}(x),$

so $d(x) = x$ for rational $x$ and $d(x) = 0$ for irrational $x$ . Then the limit of $d$ at $0$ exists, with

$\lim_{x \to 0} d(x) = 0 ,$

and at every $c \ne 0$ the function $d$ has no limit.

The point of the example. The factor $\mathbf{1}_{\mathbb{Q}}$ has a limit nowhere; multiplying it by $x$ repairs exactly one point, and only that one. The repair at $0$ is the squeeze theorem (If $f \le g \le h$ near $c$ and $f$ and $h$ have the same limit at $c$ , then so does $g$ ) applied to $-|x| \le d(x) \le |x|$ ; the failure elsewhere is the same two-sequence argument as in The indicator of $\mathbb{Q}$ has a limit at no point of $\mathbb{R}$ , now with image limits $c$ and $0$ , which are distinct precisely because $c \ne 0$ .

Facts & Assumptions

Given: The canonical copy $\mathbb{Q} \subseteq \mathbb{R}$ of the rationals, the irrationals $X = \mathbb{R} \setminus \mathbb{Q}$ , the function $d(x) = x \cdot \mathbf{1}_{\mathbb{Q}}(x)$ , and a real $c \ne 0$ .

[L1]

The values of $d$ : $d(x) = x$ for $x \in \mathbb{Q}$ and $d(x) = 0$ for $x \in X$ ; every real lies in exactly one of $\mathbb{Q}$ and $X$ (The indicator of $\mathbb{Q}$ has a limit at no point of $\mathbb{R}$ ).

[L2]

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} f(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 $|f(x) - P| < \varepsilon$ .

[L3]

Squeeze theorem: if $f \le g \le k$ on $A \cap N^{*}_{\eta}(c)$ for some real $\eta > 0$ and the limits of $f$ and of $k$ at $c$ exist and are equal to $L$ , then the limit of $g$ at $c$ exists and equals $L$ (If $f \le g \le h$ near $c$ and $f$ and $h$ have the same limit at $c$ , then so does $g$ ).

[L4]

Nonexistence criterion (A function has no limit at $c$ as soon as two sequences in $A \setminus \{c\}$ tending to $c$ give different limits of the values).

[L5]

For every real $c$ there are a sequence $(q_k)$ with all terms in $\mathbb{Q} \setminus \{c\}$ and a sequence $(u_k)$ with all terms in $X \setminus \{c\}$ , both converging to $c$ . This is exactly what is established in the course of The indicator of $\mathbb{Q}$ has a limit at no point of $\mathbb{R}$ , from density (Both $\mathbb{Q}$ and $\mathbb{R} \setminus \mathbb{Q}$ are dense in $\mathbb{R}$ , and every nonempty open subset of $\mathbb{R}$ is uncountable, 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 $\mathbb{R}$ , The rationals embed densely in the reals) and the sequential characterisation of the closure (A point lies in the closure of $A \subseteq \mathbb{R}$ iff some sequence in $A$ converges to it, so a subset of $\mathbb{R}$ is closed iff it is sequentially closed, Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals); the countable choice spent there is inherited here.

[L6]

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}$ ).

[L7]

Absolute value: $|u| \ge 0$ ; $-|u| \le u \le |u|$ ; $|u| = u$ for $u \ge 0$ ; $|0| = 0$ (Basic properties of the absolute value). Order arithmetic: trichotomy and totality; $0 < 1$ , so $2 > 0$ and $\varepsilon/2 < \varepsilon$ for $\varepsilon > 0$ (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field).

[L8]

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

Verification

technique · direct

1.1

For every $x \in \mathbb{R}$ , $-|x| \le d(x) \le |x|$ : if $x \in \mathbb{Q}$ then $d(x) = x$ and $-|x| \le x \le |x|$ ; if $x \in X$ then $d(x) = 0$ and $-|x| \le 0 \le |x|$ .

L1L7

1.2

Every real is a limit point of $\mathbb{R}$ ; in particular $0$ and the given $c$ are.

1.3

The functions $x \mapsto -|x|$ and $x \mapsto |x|$ have limit $0$ at $0$ : given a real $\varepsilon > 0$ take $\delta := \varepsilon$ ; every $x$ with $0 < |x - 0| < \delta$ satisfies $\bigl| |x| - 0 \bigr| = |x| < \varepsilon$ and $\bigl| -|x| - 0 \bigr| = |x| < \varepsilon$ .

L2L7

2.1

The three functions satisfy $-|x| \le d(x) \le |x|$ on all of $\mathbb{R}$ , in particular on $\mathbb{R} \cap N^{*}_{1}(0)$ , and the outer two have limit $0$ at $0$ ; since $0$ is a limit point of $\mathbb{R}$ , the squeeze theorem [L3] gives that the limit of $d$ at $0$ exists and equals $0$ .

step 1.1step 1.2step 1.3L3

2.2

Fix the real $c \ne 0$ . By [L5] there are a sequence $(q_k)$ with all terms in $\mathbb{Q} \setminus \{c\}$ and a sequence $(u_k)$ with all terms in $X \setminus \{c\}$ , both converging to $c$ .

step 1.2L5choose

3.1

By [L1], $d(q_k) = q_k$ for every $k$ , so the image sequence $(d(q_k))$ is $(q_k)$ itself and converges to $c$ ; and $d(u_k) = 0$ for every $k$ , so that image sequence is constant and converges to $0$ . Since $c \ne 0$ , the two limits are distinct, and both sequences have all their terms in $\mathbb{R} \setminus \{c\}$ and converge to $c$ ; by [L4] the function $d$ has no limit at $c$ .

step 2.2L1L4L7L8

4.1

So the limit of $d$ exists at $0$ , with value $0$ , and fails to exist at every other real: $d$ has a limit at exactly one point.

step 2.1step 3.1∎

Remarks

Why $0$ is the exceptional point. The squeeze bound $|d(x)| \le |x|$ is useful only where $|x|$ is small, that is near $0$ ; at any other $c$ the two bounding functions have limit $|c| \ne 0$ and $-|c|$ , which are different, so the squeeze theorem says nothing there. That is not an accident of the proof: the two-sequence argument shows the limit genuinely fails at every such $c$ .
The value $d(0) = 0$ happens to equal the limit, since $0$ is rational, so $d$ satisfies at $0$ the equality that FALSE: $\lim_{x \to c} f(x) = f(c)$ whenever both sides exist shows is not automatic. It is the only point of $\mathbb{R}$ at which $d$ does so.
Contrast with $\psi(1/x)$ . There the oscillation is bounded and the failure is confined to a single point, $0$ , with the multiplication by $x$ repairing precisely that point ( $x\,\psi(1/x) \to 0$ as $x \to 0$ , by the squeeze theorem). Here the failure is everywhere and the multiplication repairs precisely one point. The two examples are the same mechanism — a bounded factor damped by a vanishing one — applied to opposite kinds of irregularity.

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: 100 results over 31 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

Dirichlet function (Wikipedia) (standard reference, not scraped)
Squeeze theorem (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)

x⋅1Q(x)x \cdot 1_{\mathbb{Q}}(x)x⋅1Q​(x) has a limit at 000 and at no other point