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.
Paths, path-connected spaces and path components
Definition
Throughout, (Intervals of : the nine order-convex forms, nondegeneracy, and length) carries the subspace topology inherited from with its usual topology (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace, The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not). It is called the unit interval.
Let be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) and let .
- A path in from to is a continuous map (Continuity of a map of topological spaces at a point and globally) with and . Its image is .
- is path-connected when for every pair there is a path in from to . A subset is a path-connected subset when the space with its subspace topology is path-connected; equivalently, when any two of its points are joined by a path whose image lies in , by the characteristic property of a map into a subspace (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).
- Write when a path in from to exists. The path component of is its equivalence class
- The empty space is path-connected, the defining condition quantifying over no pair of points, and so is every one-point space, the constant path joining its point to itself.
is an equivalence relation on , and the obligation is discharged here, so that "equivalence class" above denotes.
Reflexive. The constant map is continuous, every preimage being or (Continuity of a map of topological spaces at a point and globally), and joins to .
Symmetric. If joins to , put . The map , , is continuous: for one has , so a ball of radius around pulls back to contain the ball of radius around (Open ball, closed ball and sphere in a metric space, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not). Hence is continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, claim 1) and joins to .
Transitive. Let join to and join to . Define by
The two clauses agree at , both giving , so is a well-defined function. The sets and are closed in and cover it, and there are two of them, so the finite closed form of the pasting lemma applies (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, claim 3). On the map is with , and on it is with ; each is continuous into , since , so the ball of radius around maps into the ball of radius around (Open ball, closed ball and sphere in a metric space, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace). So both restrictions are continuous by Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous claim 1, hence is continuous, and it joins to .
The path components partition , being the classes of an equivalence relation, and each is a path-connected subset of : two points of are joined to , hence to each other by the transitivity construction above, and the resulting path has image inside : if is a path from and , then is a path from to , continuous because satisfies and is therefore continuous into by the ball criterion used above, so every point of the image is itself joined to .
Remarks
-
Why the unit interval and not an arbitrary closed bounded interval. Any with would give the same relation, since carries onto and is continuous with continuous inverse. Fixing removes a parameter from every statement below and costs nothing.
-
A path is a map, not a subset. The image is a subset of , but the path is the map: two different paths may have the same image, and the concatenation above depends on the maps rather than on their images. Nothing in this library identifies a path with its image.
-
Path components are not asserted to be closed, or open, or to coincide with components. Each of those is false in general, and each is taken up separately on this page. What is proved here is only that they partition and that each is path-connected.
-
The finiteness in the pasting lemma is what makes concatenation legal. The cover has two members. An infinite closed cover would not do, and the standing warning is covered by its closed singletons: every restriction of the indicator of is continuous and the map is not, so the closed pasting lemma needs finiteness; this is worth naming here because the temptation to concatenate infinitely many paths is exactly what fails for the zigzag curve later on this page.
Depends on
Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets
Continuity of a map of topological spaces at a point and globally
Intervals of : the nine order-convex forms, nondegeneracy, and length
Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace
The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded
The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
Open ball, closed ball and sphere in a metric space
Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not
Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous
Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison