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.
Refinements, locally finite families, point-finite families, and star refinements
Definition
Let be a topological space. A family of subsets of is a refinement of a family when every is contained in some . It is an open refinement when, additionally, every is open. A refinement of a cover need not itself cover ; when it does, it is called a refining cover.
A family of subsets of is locally finite when every point has a neighbourhood meeting only finitely many members of . It is point-finite when every belongs to only finitely many members of . Local finiteness implies point-finiteness: a neighbourhood of meeting only finitely many members contains , so every member containing is among those finitely many. The converse is not part of the definition and can fail.
For a family and a subset , its star about is A cover is a star refinement of a cover when for every there is with .
Remarks
The word “neighbourhood” has the library convention from Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open: it need not itself be open. Replacing it by an open neighbourhood gives the same local-finiteness condition, because every neighbourhood contains an open one about the same point.
Depends on
Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right
Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open
Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison