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.
Equicontinuity on a topological domain and pointwise relative compactness
Definition
Let be a topological space, let be a metric space, and let .
The family is equicontinuous at if, for every , there is a neighbourhood of such that
for every and every . It is equicontinuous if it is equicontinuous at every . The same neighbourhood must serve every member of the family. The empty family is equicontinuous, and when the pointwise condition is vacuous.
For , write . The family is pointwise relatively compact if the closure is a compact subset of for every . Thus an empty family is pointwise relatively compact because the empty set is compact, and an empty domain again makes the condition vacuous.
Depends on
Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open
Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric
Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right
Continuity of a map of topological spaces at a point and globally
Interior, closure, boundary, exterior, derived set and isolated point in a topological space