TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-27 (gpt-5)

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 Dirichlet function is continuous at no point of $R$ , and Thomae's function is continuous at every irrational and at no rational, so its set of continuity points is exactly the set of irrationals and its oscillation at $c$ equals $t (c)$

Statement

Let $1_{Q}$ and $t$ be the Dirichlet and Thomae functions (The Dirichlet function $1_{Q}$ , and Thomae's function $t$ with $t (x) = 1 / q$ at a rational $x = p / q$ in lowest terms with $q \geq 1$ and $t (x) = 0$ at every irrational $x$ ), and write $q (x)$ for the least denominator of a rational $x$ , so that $t (x) = 1 / ι (q (x))$ there and $t (x) = 0$ at every irrational $x$ . Then:

$1_{Q}$ is continuous at no point of $R$ (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point);
$ω_{t} (c) = t (c)$ for every real $c$ (The oscillation $ω_{f} (S) = \sup {∣ f (x) - f (y) ∣ : x, y \in S}$ of $f$ on a set and the oscillation $ω_{f} (c) = \inf_{δ > 0} ω_{f} (A \cap N_{δ} (c))$ at a point, both taken in the extended reals);
$t$ is continuous at every irrational and discontinuous at every rational, so its set of continuity points is exactly $R ∖ Q$ .

Claim 1 duplicates a companion examples-page argument on purpose. The examples-page proof that the Dirichlet function is nowhere continuous lives on a leaf page of the library, so later A-page items cannot cite it directly. The claim is needed here, and on later pages, as a citable theorem-level statement, so it is proved again rather than quoted. The two statements are the same, and no originality is claimed for the repeated proof. The same duplication pattern is used elsewhere in this page family for examples whose argument also has to be available in A-page form.

Facts & Assumptions

Given: The Dirichlet function $1_{Q}$ and Thomae's function $t$ , and a real $c$ ; $N \subseteq Z \subseteq Q \subseteq R$ are the canonical copies and $ι (q) = q \cdot 1_{R}$ .

[A1]

$1_{Q} (x) = 1$ for $x \in Q$ and $0$ otherwise; $t (x) = 1 / ι (q (x)) \in (0, 1]$ for $x \in Q$ and $t (x) = 0$ otherwise, where $q (x) = \min {q \geq 1 : ι (q) x \in Z}$ (The Dirichlet function $1_{Q}$ , and Thomae's function $t$ with $t (x) = 1 / q$ at a rational $x = p / q$ in lowest terms with $q \geq 1$ and $t (x) = 0$ at every irrational $x$ ).

[L1]

Both $Q$ and $R ∖ Q$ are dense in $R$ , so every $N_{δ} (y)$ contains a rational and an irrational (Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $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, The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ , The rationals embed densely in the reals).

[L2]

For every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ , written $⌊ x ⌋$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ); consequently no integer lies strictly between two consecutive integers.

[L3]

For every real $η > 0$ there is a natural $N \geq 1$ with $1 / ι (N) < η$ ; and $ι$ is positive and strictly increasing on the naturals $\geq 1$ , so $1 \leq q \leq N$ gives $ι (q) \leq ι (N)$ and $1 / ι (N) \leq 1 / ι (q)$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing).

[L4]

A nonempty finite set of reals presented as ${a_{0}, \dots, a_{n}}$ has a minimum (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[L5]

$ω_{f} (S) = \sup {∣ f (x) - f (y) ∣ : x, y \in S}$ and $ω_{f} (c) = \inf {ω_{f} (N_{δ} (c)) : δ > 0}$ for $f$ defined on all of $R$ , both computed in $\overline{R}$ , where every set has a supremum and an infimum; $f$ is continuous at $c$ if and only if $ω_{f} (c) = 0$ (The oscillation $ω_{f} (S) = \sup {∣ f (x) - f (y) ∣ : x, y \in S}$ of $f$ on a set and the oscillation $ω_{f} (c) = \inf_{δ > 0} ω_{f} (A \cap N_{δ} (c))$ at a point, both taken in the extended reals, The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined, Every subset of $\overline{R}$ has a least upper bound and a greatest lower bound in $\overline{R}$ , agreeing with the real supremum and infimum on nonempty sets bounded in $R$ , $f : A \to R$ is continuous at $c \in A$ if and only if $ω_{f} (c) = 0$ ).

[L6]

If $0 \leq u \leq M$ and $0 \leq v \leq M$ , then $- M \leq u - v \leq M$ ; consequently $∣ u - v ∣ \leq M$ , by the two cases $u - v \geq 0$ and $u - v < 0$ .

Proof

technique · cases

1.1

Claim 1. Let $c$ be real and let $δ > 0$ be real. The neighbourhood $N_{δ} (c)$ contains a rational $u$ and an irrational $v$ , and $1_{Q} (u) - 1_{Q} (v) = 1 - 0 = 1$ ; since $1_{Q} (c)$ is $0$ or $1$ , one of $∣ 1_{Q} (u) - 1_{Q} (c) ∣$ and $∣ 1_{Q} (v) - 1_{Q} (c) ∣$ equals $1$ . So the continuity condition at $c$ fails for $ε = 1$ , no $δ$ witnessing it, and $1_{Q}$ is continuous at no point.

A1L1

1.2

A separation estimate. For a real $c$ and a natural $q \geq 1$ put $m : = ⌊ ι (q) c ⌋$ and define $d_{q} (c) : = 1 / ι (q)$ if $ι (q) c = m$ , and $d_{q} (c) : = \min {ι (q) c - m, m + 1 - ι (q) c} / ι (q)$ otherwise. In both cases $d_{q} (c) > 0$ .

L2L3construct

1.3

A lower bound. For every real $δ > 0$ the neighbourhood $N_{δ} (c)$ contains an irrational $v$ , and $c \in N_{δ} (c)$ , so $ω_{t} (N_{δ} (c)) \geq ∣ t (c) - t (v) ∣ = t (c)$ ; taking the infimum over $δ$ gives $ω_{t} (c) \geq t (c)$ .

A1L1L5

2.1

With $d_{q} (c)$ as in step 1.2: for every integer $p$ with $p / ι (q) \neq c$ one has $∣ c - p / ι (q) ∣ \geq d_{q} (c)$ . If $ι (q) c = m$ then $p \neq m$ , so $∣ ι (q) c - p ∣ = ∣ m - p ∣ \geq 1$ ; otherwise $m < ι (q) c < m + 1$ , and $p \leq m$ gives $ι (q) c - p \geq ι (q) c - m$ while $p \geq m + 1$ gives $p - ι (q) c \geq m + 1 - ι (q) c$ . Dividing by $ι (q) > 0$ gives the claim.

step 1.2L2L3

2.2

For a real $c$ and a natural $N \geq 1$ put $δ_{N} (c) : = \min {d_{1} (c), \dots, d_{N} (c)}$ , the minimum of a nonempty finite set of positive reals, so $δ_{N} (c) > 0$ .

step 1.2L4construct

3.1

If $x$ is rational with $0 < ∣ x - c ∣ < δ_{N} (c)$ then $q (x) > N$ and hence $t (x) < 1 / ι (N)$ . Indeed $x = p / ι (q)$ with $q : = q (x)$ and $p : = ι (q) x$ ; if $q \leq N$ then $p / ι (q) = x \neq c$ , so step 2.1 gives $∣ c - x ∣ \geq d_{q} (c) \geq δ_{N} (c)$ , contrary to the hypothesis. So $q (x) > N$ , and $t (x) = 1 / ι (q (x)) < 1 / ι (N)$ because $ι$ is strictly increasing.

step 2.1step 2.2A1L3

4.1

An upper bound for $t$ near $c$ . Let $ε > 0$ be real, take $N \geq 1$ with $1 / ι (N) < ε$ and put $δ : = δ_{N} (c)$ . Every $x \in N_{δ} (c)$ satisfies $0 \leq t (x) \leq M$ where $M : = \max {t (c), ε}$ : for $x = c$ this is $t (c) \leq M$ ; for $x \neq c$ rational it is $t (x) < 1 / ι (N) < ε \leq M$ by step 3.1; and for $x$ irrational it is $t (x) = 0$ .

step 3.1A1L3L6

5.1

Hence $ω_{t} (N_{δ} (c)) \leq M$ with $δ$ and $M$ as in step 4.1, since $∣ t (x) - t (y) ∣ \leq M$ for all $x, y \in N_{δ} (c)$ , so $M$ is an upper bound of the set whose supremum $ω_{t} (N_{δ} (c))$ is; and therefore $ω_{t} (c) \leq M = \max {t (c), ε}$ .

step 4.1L5L6

6.1

Claim 2 now follows in the two cases of the value $t (c)$ , which are exactly the two cases of the position of $c$ . If $c$ is rational then $t (c) > 0$ , and applying step 5.1 with the admissible choice $ε : = t (c)$ gives $ω_{t} (c) \leq \max {t (c), t (c)} = t (c)$ ; with step 1.3 this gives $ω_{t} (c) = t (c)$ .

step 5.1step 1.3A1assume-case rat

6.2

If $c$ is irrational then $t (c) = 0$ , and step 5.1 gives $ω_{t} (c) \leq \max {0, ε} = ε$ for every real $ε > 0$ ; since also $ω_{t} (c) \geq 0$ , an extended real that is $\leq ε$ for every positive real $ε$ and $\geq 0$ must be $0$ , so $ω_{t} (c) = 0 = t (c)$ .

step 5.1step 1.3A1L5assume-case irr

7.1

Every real is rational or irrational and not both, so steps 6.1 and 6.2 establish claim 2 for every real $c$ .

step 6.1step 6.2cases-exhaustive

8.1

Claim 3 follows from claim 2: $t$ is continuous at $c$ exactly when $ω_{t} (c) = 0$ , that is exactly when $t (c) = 0$ , that is exactly when $c$ is irrational. So the continuity set of $t$ is $R ∖ Q$ and its discontinuity set is $Q$ .

step 7.1A1L5∎

Remarks

What claim 2 adds beyond claim 3. Continuity at a point is the vanishing of the oscillation there, so claim 3 is the special case of claim 2 recording where the value is $0$ . The value itself is used on the companion page, where the oscillation of $t$ is computed at particular points, and it shows that the failure of continuity at a rational is exactly as large as the value of $t$ there: small denominators are the bad points.
The continuity set of $t$ is $G_{δ}$ , as it must be. The irrationals form a $G_{δ}$ set ( $Q$ is $F_{σ}$ , meager and not $G_{δ}$ , while the irrationals are $G_{δ}$ , residual and not $F_{σ}$ ), in agreement with For $f : A \to R$ the set of points of $A$ at which $f$ is discontinuous is the intersection with $A$ of an $F_{σ}$ subset of $R$ , and the set of points at which $f$ is continuous is the intersection with $A$ of a $G_{δ}$ subset; for $A = R$ the two sets are $F_{σ}$ and $G_{δ}$ outright. The reverse arrangement is impossible: no function is continuous at every rational and discontinuous at every irrational, because $Q$ is not $G_{δ}$ (No function $R \to R$ is continuous at every rational and discontinuous at every irrational, because $Q$ is not $G_{δ}$ ).
No choice principle is spent. The separation estimate of step 1.2 is written down from $⌊ ι (q) c ⌋$ , the minimum of step 2.1 is the minimum of an explicitly listed finite set, and the least denominator $q (x)$ is a least element. Density supplies points, and it is used only in the form "every neighbourhood meets the set", never to build a sequence.

Depends on

Used by

Dependency tree · two levels

67 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

Thomae's function (Wikipedia) (standard reference, not scraped)
Dirichlet function (Wikipedia) (standard reference, not scraped)

The Dirichlet function is continuous at no point of RR, and Thomae's function is continuous at every irrational and at no rational, so its set of continuity points is exactly the set of irrationals and its oscillation at cc equals t(c)t(c)