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.
Perfect subset of : closed with no isolated points
Definition
A set is perfect when
- is closed (Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen), and
- has no isolated points (Limit point, isolated point, adherent point, derived set, and dense subset of ): no admits a real with .
Equivalently, is closed and . By Limit point, isolated point, adherent point, derived set, and dense subset of , a point of is isolated in exactly when it is not a limit point of , so "no point of is isolated in " says precisely that every point of is a limit point of , that is, . Combined with the characterisation of closedness as (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), a perfect set is exactly a set with , though only the two conditions above are used below.
Remarks
-
Both conditions are needed and neither implies the other. The set is closed and has the isolated point , so it is not perfect ( is closed, has an isolated point, and is not perfect ↗); the open interval has no isolated points and is not closed, so it is not perfect either.
-
is perfect, vacuously: it is closed and has no points at all, hence no isolated ones. This is why Every nonempty perfect subset of is uncountable carries the hypothesis that is nonempty: the empty set is perfect and countable.
-
A nonempty perfect set is forced to be large. It is uncountable (Every nonempty perfect subset of is uncountable), and the simplest examples are the nondegenerate closed intervals (Every nondegenerate closed interval is perfect, giving a second proof that it is uncountable ↗). A perfect set need not contain any interval, the Cantor set being the standard example of that; it is not constructed anywhere in this library, and the statement is recorded here as orientation only, on the references above.
Depends on
Limit point, isolated point, adherent point, derived set, and dense subset of
Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen
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