LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Nonempty closed connected 1-manifolds are circles

Statement

Assume ${A C}_{ω}$ . Every nonempty closed connected smooth $1$ -manifold is diffeomorphic to the circle $S^{1} = R / Z$ with its standard smooth structure (The circle as $S^{1} = R / Z$ with basepoint $[0]$ , Diffeomorphisms and local diffeomorphisms of manifolds). Here closed means compact with empty boundary; the empty manifold is excluded because it is connected under Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets but is not diffeomorphic to a circle.

Facts & Assumptions

Given: A nonempty closed connected smooth $1$ -manifold $M$ , and ${A C}_{ω}$ .

[A1]

${A C}_{ω}$ : every countable family of nonempty sets has a choice function (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

Every compact smooth $1$ -manifold $W$ , possibly with boundary, is diffeomorphic to a finite disjoint union of copies of the circle $S^{1}$ and of the closed interval $[0, 1]$ ; a diffeomorphism of manifolds with boundary maps $\partial W$ onto the boundary of the target, and each closed-interval component contributes exactly its two endpoints to that boundary (Boundary of a compact 1-manifold has even cardinality).

[F2]

A closed smooth manifold is by definition a compact smooth manifold with empty boundary (Smooth manifolds and their smooth charts, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right); in particular $\partial M = \emptyset$ .

[F3]

The circle is $S^{1} = R / Z$ with the quotient topology and its standard smooth structure, and a diffeomorphism is a bijective smooth map whose inverse is smooth (The circle as $S^{1} = R / Z$ with basepoint $[0]$ , Diffeomorphisms and local diffeomorphisms of manifolds).

Proof

1.1A1F1F2algebra

By [F2] the manifold $M$ is compact with $\partial M = \emptyset$ , so [F1] provides a diffeomorphism from $M$ onto a finite disjoint union $⨆_{i \in F} S_{i}^{1} ⊔ ⨆_{j \in G} [0, 1]_{j}$ ; a diffeomorphism of manifolds with boundary carries boundary to boundary, and the boundary of the target is the union of the two endpoints of each interval component, so $\emptyset = \partial M$ corresponds to $⨆_{j \in G} {0, 1}$ and forces $G = \emptyset$ .

2.1F1F3step 1.1algebra∎

Consequently $M$ is diffeomorphic to $⨆_{i \in F} S_{i}^{1}$ , a disjoint union of $∣ F ∣$ copies of the circle. Each circle is a nonempty connected component of that disjoint union, so the union is connected only when $∣ F ∣ \leq 1$ , and $M$ is nonempty, so $∣ F ∣ = 1$ ; hence $M$ is diffeomorphic to the standard circle $S^{1}$ , the model $R / Z$ of [F3], as claimed.

Depends on

Used by

Dependency tree · two levels

37 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

John Milnor, Topology from the Differentiable Viewpoint (complete 76-page PDF, including the appendix Classifying 1-manifolds) (standard reference, not scraped)