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: $d(x,y) = 0$ iff $x = y$, 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
Used by
- For finite discrete X and compact metric Y, the whole space C(X,Y) is compact Example
- The compact-open and pointwise topologies agree on an equicontinuous family Lemma
- The pointwise closure of an equicontinuous family is equicontinuous and consists of continuous maps Lemma
- Every compact compact-open family is pointwise relatively compact Proposition
- Topological-domain equicontinuity agrees with metric equicontinuity on a metric domain Proposition
- A compact compact-open family is equicontinuous on a locally compact Hausdorff domain Theorem
- Under Choice, pointwise closure is compact exactly when every coordinate set has compact closure Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 39 results over 11 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
- Topology, second edition, Sections 45 and 47 (standard reference, not scraped)