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.
is continuous at and at no other point
Example
Let be the indicator of the rationals (The indicator of is continuous at no point of ) and put
so for rational and for irrational . Then:
- is continuous at (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point);
- is not continuous at any .
So the set of points of continuity of a real function can be a single point. Together with The indicator of is continuous at no point of , where that set is empty, this shows how little the set of continuity points is constrained by the mere existence of the function.
The point of the example. Continuity at compares with , and the two branches of agree only where . Multiplying the indicator by damps the jump: near both branches are small, so the discrepancy is at most ; away from the discrepancy is at least on every neighbourhood, because each branch is realised arbitrarily close to .
Facts & Assumptions
Given: The canonical copy of the rationals with complement , and with for and for .
Continuity at , in the form of Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point: for every real there is a real with whenever ; and it fails at as soon as some real admits, for every real , a real with and (The -neighbourhood and the punctured -neighbourhood of a point of ).
Both and are dense in , so every meets each of them (Both and are dense in , and every nonempty open subset of 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).
is by definition the complement , so every real lies in exactly one of and ; hence is a well-defined function, and for every real (Basic properties of the absolute value, The indicator of is continuous at no point of ).
Absolute value and order: and exactly when (Basic properties of the absolute value); the reverse triangle inequality , hence (The reverse triangle inequality); and the minimum of a two-element set of reals exists and is one of the two (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set, Ordered field).
Verification
is well defined and satisfies for every real : on one has and on one has . Also , so .
Claim 2, the setup. Let be real, put by [L4], and let a real be given. Put by [L4].
Claim 1. Let a real be given and take . Every real with satisfies by step 1.1. So is continuous at .
By [L2] the neighbourhood meets and meets : fix and , so and , with and .
The rational case. Suppose , so . Take : then and .
The irrational case. Suppose , so . Take : then , and by [L4] and step 2.2, so .
By [L3] the two cases of steps 3.1 and 3.2 are exhaustive, so for every real some with has ; by [L1] the function is not continuous at . Since was arbitrary, claim 2 holds, and with step 2.1 the set of points of continuity of is exactly .
Remarks
-
Where the damping factor does its work. The estimate of step 1.1 is the whole of claim 1, and it is available only because the two branches of agree at . Replacing by any function vanishing at and continuous there gives the same conclusion at ; replacing it by a nonzero constant gives The indicator of is continuous at no point of back.
-
The choice of is what makes the irrational case work. Without shrinking to the rational point near could be close to , and then would be small; the shrinking keeps away from by at least .
-
This example is choice free, for the same reason as The indicator of is continuous at no point of : density is used only in the form "every neighbourhood meets the set", never to build a sequence.
Depends on
- The indicator of $\mathbb{Q}$ is continuous at no point of $\mathbb{R}$
- Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$: the $\varepsilon$-$\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point
- The reverse triangle inequality
- 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
- The $\varepsilon$-neighbourhood and the punctured $\varepsilon$-neighbourhood of a point of $\mathbb{R}$
- Maximum and minimum of a set
- Every nonempty finite set of reals has a maximum and a minimum
- Basic properties of the absolute value
- Ordered field
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: 76 results over 21 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)
- Continuous function (Wikipedia) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §3.2 (standard reference, not scraped)
- E. Boman and R. Rogers, An Analytic Definition of Continuity (standard reference, not scraped)