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.
Components of a topological manifold are open and at most countable
Statement
Let be a topological manifold. Then every connected component of is open. Moreover the set of connected components of is at most countable.
Facts & Assumptions
Given: A topological manifold .
A topological manifold is second countable (Topological manifolds without boundary: Hausdorff, second-countable, and locally Euclidean spaces).
A topological manifold is locally path connected (Topological manifolds are locally compact and locally path connected).
In a locally connected space, the connected components of every open set are open; applied to the open set itself, this makes components of open (A space is locally connected exactly when every component of every open subspace is open; in that case the components of the space itself are clopen).
Connected components partition the space and are pairwise disjoint (The components of a space are its maximal connected subsets, they partition it, and each of them is closed).
Every path-connected open neighbourhood is connected, so local path connectedness implies local connectedness.
Proof
By [F2] every point of has a path-connected open neighbourhood; by [A1] such a neighbourhood is connected, so is locally connected. Therefore [L1] applied to the open set shows that every connected component of is open.
Because is second countable by [F1], choose a countable basis [F1, step 1.1, choose] . Let be the set of connected components of . By step 1.1 each is a nonempty open set, so there exists at least one index with and . Choose the least such index and call it .
If and , then . [L2, step 2.1] Since components are disjoint by [L2], this forces . Thus is injective from into , so is at most countable.
Step 1.1 proves openness of components and step 3.1 proves that there are at most countably many of them.
Depends on
- Topological manifolds without boundary: Hausdorff, second-countable, and locally Euclidean spaces
- Topological manifolds are locally compact and locally path connected
- The components of a space are its maximal connected subsets, they partition it, and each of them is closed
- A space is locally connected exactly when every component of every open subspace is open; in that case the components of the space itself are clopen
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Rob van der Vorst, Introduction to differentiable manifolds, §1 (standard reference, not scraped)
- Nigel Hitchin, Differentiable Manifolds, §2.2 (standard reference, not scraped)