PropositionStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-29

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.

Countable disjoint unions of fixed-dimensional smooth manifolds are smooth manifolds

Statement

Let $I$ be an at most countable set with a fixed enumeration, and for each $i \in I$ let $M_{i}$ be a smooth $n$ -manifold presented with a fixed smooth atlas and a fixed finite or countable listing of a basis of its topology. Then the disjoint union $X : = ⨆_{i \in I} M_{i}$ with the disjoint union topology is a smooth $n$ -manifold: the charts of the members transported by the canonical injections form a smooth atlas whose generated maximal atlas depends only on the smooth structures of the $M_{i}$ . If instead only the existence of second-countable topologies on the members is assumed, then selecting one basis per member uses ${A C}_{ω}$ ; the countability of $I$ is essential, and no claim is made for an uncountable index set.

Facts & Assumptions

Given: An at most countable set $I$ with a fixed enumeration, and for each $i \in I$ a smooth $n$ -manifold $M_{i}$ with a fixed finite or countable listing of a basis $B_{i}$ of its topology and a smooth atlas $A_{i}$ .

[F1]

The disjoint union topology declares $U \subseteq ⨆_{i} M_{i}$ open exactly when every trace $U \cap κ_{i} [M_{i}]$ is open in $M_{i}$ , and each $κ_{i}$ is an injective embedding with clopen image (The disjoint union (coproduct) $⨆_{i} X_{i}$ with the final topology of the canonical injections: a set is open exactly when each of its traces is).

[F3]

A chart is a homeomorphism of an open domain onto an open subset of $R^{n}$ (Manifold charts, coordinate domains, and coordinate functions), and two charts are smoothly compatible when their domains are disjoint or both transition maps are smooth (Smoothly compatible charts and the smoothness of Euclidean transition maps).

[F4]

A smooth atlas is a set of pairwise smoothly compatible charts whose domains cover the manifold (Smooth atlases).

[F5]

A topological space is second countable when its topology has an at most countable basis (Second countability: an at most countable basis for the topology).

[L1]

Two atlases generate the same maximal atlas exactly when their union is a smooth atlas (Each smooth atlas is contained in a unique maximal smooth atlas).

Proof

technique · direct

1.1

$X$ is Hausdorff: two points of one summand are separated inside $M_{i}$ , which is Hausdorff, and points of distinct summands lie in the disjoint clopen images $κ_{i} [M_{i}]$ and $κ_{j} [M_{j}]$ supplied by [F1]. For $p = κ_{i} (x)$ take a chart $(V, φ)$ of $M_{i}$ at $x$ ; the transported map $κ_{i} (V) \to φ (V)$ , $(x, i) \mapsto φ (x)$ , is a homeomorphism onto the open set $φ (V) \subseteq R^{n}$ by [F1] and [F3], so $X$ is locally Euclidean of dimension $n$ . The supplied listings make the union ${κ_{i} [B] : i \in I, B \in B_{i}}$ at most countable by a diagonal enumeration over the fixed enumeration of $I$ and the fixed listing of each $B_{i}$ ; it is a basis of $X$ because [F1] says openness is checked tracewise and each $B_{i}$ is a basis of $M_{i}$ . Hence $X$ is second countable by [F5] and is a topological $n$ -manifold.

givenF1F3F5

1.2

Two transported charts from one summand are compatible because their transitions are the corresponding transitions inside the smooth atlas $A_{i}$ ; two transported charts from distinct summands have disjoint domains and are compatible by the disjoint clause of [F3]. Hence the set of all transported charts is pairwise smoothly compatible, and [F4] makes it a smooth atlas on $X$ .

givenF3F4

2.1

The transported charts $(κ_{i} [V], φ \circ κ_{i}^{- 1})$ for $(V, φ) \in A_{i}$ are charts of $X$ by step 1.1, and their domains cover $X$ because each $A_{i}$ covers $M_{i}$ by [F4].

givenF4step 1.1

3.1

If $A_{i}^{'}$ is another smooth atlas of $M_{i}$ generating the same structure for each $i$ , then each $A_{i} \cup A_{i}^{'}$ is a smooth atlas by [L1]; the union of the two transported atlases has cross transitions that are transported smooth transitions exactly as in step 1.2, so it is a smooth atlas, and [L1] gives the same maximal atlas on $X$ . The structure therefore depends only on the smooth structures of the $M_{i}$ ; the ${A C}_{ω}$ cost of choosing bases from mere existence of second countability is stated, not incurred, in this proof.

givenL1step 1.2∎

Depends on

Used by

A countable disjoint union of lines is a smooth manifold Example
An arbitrary disjoint union of second-countable manifolds need not be second-countable False statement
A map from a disjoint union is smooth iff each restriction is smooth Proposition

Dependency tree · two levels

23 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, §2 (standard reference, not scraped)
Nigel Hitchin, Differentiable Manifolds, §2.3 (standard reference, not scraped)