ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)

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.

The cylinder and the Mobius band as quotients of the square by $(0,y) \sim (1,y)$ and by $(0,y) \sim (1, 1-y)$ , both by a closed quotient map

Example

Let $S := [0,1] \times [0,1]$ be the unit square, which carries one topology by claim 1 of Products commute with subspaces; for infinite nonempty families, the closure identity $\overline{\prod A_i}=\prod \overline{A_i}$ uses the Axiom of Choice (For $n \ge 1$ the product topology on $n$ copies of the usual topology of $\mathbb{R}$ is the metric topology of $d_\infty$ on $\mathbb{R}^n$ , and hence also of $d_1$ and $d_2$ , so $\mathbb{R}^n$ as a product and $\mathbb{R}^n$ as a metric space are one space, 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, Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length). Define two relations on $S$ , in each case leaving every point not on the two vertical edges alone:

$\text{cylinder:}\quad (0,y) \sim_{\mathrm{c}} (1,y); \qquad\qquad \text{Mobius band:}\quad (0,y) \sim_{\mathrm{m}} (1, 1-y) \qquad (y \in [0,1]).$

Precisely, $\sim_{\mathrm{c}}$ has as classes the pairs $\{(0,y),(1,y)\}$ and the singletons $\{(s,t)\}$ with $0 < s < 1$ ; $\sim_{\mathrm{m}}$ has as classes the pairs $\{(0,y),(1,1-y)\}$ and the same singletons. Write $M_{\mathrm{c}} := S/\!\sim_{\mathrm{c}}$ (the cylinder) and $M_{\mathrm{m}} := S/\!\sim_{\mathrm{m}}$ (the Mobius band), each with the quotient topology (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection) and canonical projection $P_{\mathrm{c}}$ , $P_{\mathrm{m}}$ . Then:

Both projections are closed quotient maps: the saturation of a closed subset of $S$ is closed, so $P_{\mathrm{c}}$ and $P_{\mathrm{m}}$ carry closed sets to closed sets (A continuous open surjection, a continuous closed surjection, and a continuous surjection admitting a continuous section are all quotient maps).
The cylinder is $(\mathbb{R}/\mathbb{Z}) \times [0,1]$ . With $T = \mathbb{R}/\mathbb{Z}$ and its open quotient map $q$ ( $\mathbb{R}/\mathbb{Z}$ : the quotient map is open, and the quotient is homeomorphic to $[0,1]$ with its endpoints identified), the map $Q_1 := q \times \mathrm{id}_{[0,1]}$ is an open quotient map $\mathbb{R} \times [0,1] \to T \times [0,1]$ and induces a homeomorphism $M_{\mathrm{c}} \cong T \times [0,1]$ (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

Nothing here claims that the cylinder and the Mobius band are different spaces. Distinguishing them needs an invariant, and the standard ones are not available at this point in the reading order (What the theory of these constructions still owes at this point in the reading order: preservation of quotient maps under products, separation beyond Hausdorff, and the invariants that tell the glued spaces apart). Both are recorded as constructions, and only the cylinder is identified with a space built earlier.

Facts & Assumptions

Given: The square $S = [0,1]\times[0,1]$ ; the relations $\sim_{\mathrm{c}}$ and $\sim_{\mathrm{m}}$ with their quotients and projections; the edges $E_0 := \{0\}\times[0,1]$ and $E_1 := \{1\}\times[0,1]$ ; $T = \mathbb{R}/\mathbb{Z}$ with projection $q$ ; the maps $Q_1 := q \times \mathrm{id} : \mathbb{R}\times[0,1] \to T \times [0,1]$ and $F_1 : \mathbb{R}\times[0,1] \to M_{\mathrm{c}}$ , $F_1(x,y) := P_{\mathrm{c}}(x - \lfloor x \rfloor,\ y)$ .

[A1]

For a quotient $Z/\!\sim$ with projection $\Pi$ : $\Pi$ is a surjection, $W$ is open exactly when $\Pi^{-1}[W]$ is open, $W$ is closed exactly when $\Pi^{-1}[W]$ is closed, and $\Pi^{-1}[\Pi[A]]$ is the saturation of $A$ (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection, The adjunction space $Y \cup_f X$ glued along a continuous map, and, for a nonempty space, the cone and the suspension as quotients of $X \times [0,1]$ ).

[A2]

$q$ is a surjective open quotient map with $q(x) = q(x')$ exactly when $x - x' \in \mathbb{Z}$ ; for every real $x$ there is exactly one integer $\lfloor x \rfloor$ with $\lfloor x\rfloor \le x < \lfloor x\rfloor + 1$ , and $\lfloor x+m\rfloor = \lfloor x \rfloor + m$ for integers $m$ ( $\mathbb{R}/\mathbb{Z}$ : the quotient map is open, and the quotient is homeomorphic to $[0,1]$ with its endpoints identified, Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$ , The integers as equivalence classes of pairs of naturals).

[L1]

A continuous closed surjection and a continuous open surjection are quotient maps (A continuous open surjection, a continuous closed surjection, and a continuous surjection admitting a continuous section are all quotient maps, clauses 1 and 2); for a quotient map $s$ and a continuous $f$ constant on its fibres there is exactly one continuous $\bar f$ with $\bar f \circ s = f$ (For a quotient map $q : X \to Y$ , a map out of $Y$ is continuous iff its composite with $q$ is; a continuous map on $X$ constant on the fibres of $q$ factors uniquely through $q$ ; and a composite of quotient maps is a quotient map, claim 2).

[L2]

A basis for a binary product is the family of boxes $U \times V$ with $U, V$ open; a map into a binary product is continuous exactly when both components are (The product set $\prod_{i \in I} X_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice).

[L3]

Restrictions of continuous maps to subspaces are continuous, composites of continuous maps are continuous, and continuity may be checked on an open cover and on a finite closed cover (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, Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).

[L4]

A subset of a closed subspace that is closed in that subspace is closed in the ambient space; a finite union of closed sets is closed; $[0,1]$ is closed in $\mathbb{R}$ and the maps $y \mapsto 1-y$ of $[0,1]$ and $t \mapsto t + c$ of $\mathbb{R}$ are homeomorphisms (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 $\mathbb{R}$ a metric space: $d(x,y) = |x-y|$ is a metric, its open balls are the intervals $(x-r, x+r)$ , and it is unbounded, Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not, Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological, For $n \ge 1$ the product topology on $n$ copies of the usual topology of $\mathbb{R}$ is the metric topology of $d_\infty$ on $\mathbb{R}^n$ , and hence also of $d_1$ and $d_2$ , so $\mathbb{R}^n$ as a product and $\mathbb{R}^n$ as a metric space are one space).

[L5]

The pasting technique of The square with opposite edges identified is homeomorphic to the product $(\mathbb{R}/\mathbb{Z}) \times (\mathbb{R}/\mathbb{Z})$ : a map defined on $\mathbb{R}$ by taking a fractional part and then applying a quotient projection that identifies the two endpoints of $[0,1]$ is continuous, because on $[m-1,m+1]$ it agrees with a map glued from two continuous pieces over the finite closed cover $\{[m-1,m],\ [m,m+1]\}$ , and the open intervals $(m-1,m+1)$ , $m \in \mathbb{Z}$ , cover $\mathbb{R}$ .

Verification

technique · direct

1.1

$E_0$ and $E_1$ are closed in $S$ : each is the trace on $S$ of a closed subset of $\mathbb{R}^2$ , namely $\{0\}\times\mathbb{R}$ and $\{1\}\times\mathbb{R}$ , whose complements are open by [L2] and [L4].

L2L4

1.2

The maps $\tau_{\mathrm{c}}(0,y) := (1,y)$ and $\tau_{\mathrm{m}}(0,y) := (1,1-y)$ are homeomorphisms $E_0 \to E_1$ , being $y \mapsto y$ and $y \mapsto 1-y$ read through the homeomorphisms $y \mapsto (0,y)$ and $y \mapsto (1,y)$ of $[0,1]$ onto $E_0$ and $E_1$ , and both are continuous with continuous inverses by [L2], [L3] and [L4].

L2L3L4

1.3

For $C \subseteq S$ the saturation of $C$ under $\sim_{\mathrm{c}}$ is $C \cup \tau_{\mathrm{c}}[C \cap E_0] \cup \tau_{\mathrm{c}}^{-1}[C \cap E_1]$ , since the only non-singleton classes are the pairs $\{(0,y),(1,y)\}$ ; the same formula with $\tau_{\mathrm{m}}$ gives the saturation under $\sim_{\mathrm{m}}$ .

givenA1

1.4

$Q_1$ is continuous, surjective and open: continuity and surjectivity are [L2] and [A2] coordinatewise, and $Q_1[U \times V] = q[U] \times V$ for $U$ open in $\mathbb{R}$ and $V$ open in $[0,1]$ , which is open by [A2] and [L2]; images of unions are unions of images. By [L1] it is an open quotient map.

A2L1L2

1.5

$Q_1(x,y) = Q_1(x',y')$ exactly when $x - x' \in \mathbb{Z}$ and $y = y'$ , by [A2]; so the restriction $E := Q_1 \restriction S$ has exactly the classes of $\sim_{\mathrm{c}}$ as its fibres, and $E$ is continuous by [L3] and surjective, since $x - \lfloor x \rfloor \in [0,1)$ by [A2].

A2L3

1.6

$F_1$ is constant on the fibres of $Q_1$ , since $x - \lfloor x \rfloor$ depends only on the class of $x$ modulo $\mathbb{Z}$ by [A2], and it is continuous by [L5] applied in the first variable, the second variable being untouched, together with [L2] and [L3].

A2L2L3L5

2.1

If $C$ is closed in $S$ then $C \cap E_0$ is closed in $E_0$ and hence in $S$ by step 1.1 and [L4], so $\tau_{\mathrm{c}}[C\cap E_0]$ is closed in $E_1$ by step 1.2 and hence in $S$ ; likewise for $\tau_{\mathrm{c}}^{-1}[C \cap E_1]$ . So by step 1.3 the saturation of $C$ is a union of three closed sets, hence closed, and $P_{\mathrm{c}}[C]$ is closed by [A1]. The same argument with $\tau_{\mathrm{m}}$ gives the statement for $P_{\mathrm{m}}$ .

step 1.1step 1.2step 1.3A1L4

2.2

By step 1.5 and [L1] applied to the quotient map $P_{\mathrm{c}}$ and the continuous $E$ , there is exactly one continuous $\bar E : M_{\mathrm{c}} \to T \times [0,1]$ with $\bar E \circ P_{\mathrm{c}} = E$ ; by step 1.6 and [L1] applied to the quotient map $Q_1$ of step 1.4 and the continuous $F_1$ , there is exactly one continuous $\bar F : T \times [0,1] \to M_{\mathrm{c}}$ with $\bar F \circ Q_1 = F_1$ .

step 1.4step 1.5step 1.6A1L1

3.1

$\bar F \circ \bar E = \mathrm{id}$ and $\bar E \circ \bar F = \mathrm{id}$ : for $(s,t) \in S$ one has $\bar F(\bar E(P_{\mathrm{c}}(s,t))) = F_1(s,t) = P_{\mathrm{c}}(s - \lfloor s \rfloor,\ t)$ , which is $P_{\mathrm{c}}(s,t)$ because $\lfloor s \rfloor = 0$ for $s \in [0,1)$ and $(0,t) \sim_{\mathrm{c}} (1,t)$ for $s = 1$ ; and for $(x,y) \in \mathbb{R}\times[0,1]$ one has $\bar E(\bar F(Q_1(x,y))) = E(x - \lfloor x\rfloor,\ y) = Q_1(x,y)$ by [A2]. Both $P_{\mathrm{c}}$ and $Q_1$ are surjective.

step 1.4step 1.5step 2.2A1A2

4.1

Claim 1 is step 2.1, and claim 2 follows from steps 2.2 and 3.1, the maps $\bar E$ and $\bar F$ being mutually inverse and continuous, hence homeomorphisms.

step 2.1step 2.2step 3.1∎

Remarks

The two constructions differ in one sign and in nothing else. They use the same square, the same two edges and the same kind of relation; the Mobius band glues the left edge to the right edge after reversing it. Claim 1 is proved for both. Claim 2 is not: it identifies the cylinder with $(\mathbb{R}/\mathbb{Z}) \times [0,1]$ , and no analogous description of the Mobius band is attempted here. Separating the two spaces would need an invariant, and none is claimed here.
Why closedness rather than openness. Neither projection is open. Take $U := \{\, (s,t) \in S : s < 1/2 \,\}$ , which is open in $S$ ; its saturation is $U \cup (\{1\} \times [0,1])$ , and that is not open in $S$ , because every neighbourhood in $S$ of the point $(1,1/2)$ contains points $(s,1/2)$ with $1/2 < s < 1$ , which lie in neither piece. So $P_{\mathrm{c}}[U]$ is not open, and the same computation applies to $P_{\mathrm{m}}$ ; this is the failure recorded in FALSE: every quotient map is an open map. Closedness holds instead because the two edges are closed and the gluing map between them is a homeomorphism, which is what step 2.1 uses.
The cylinder is a product and the Mobius band is not built as one. Claim 2 writes $M_{\mathrm{c}}$ as $T \times [0,1]$ ; no analogous description is attempted for $M_{\mathrm{m}}$ , and none is available at this point in the reading order.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 154 results over 29 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

Mobius strip (Wikipedia) (standard reference, not scraped)
Cylinder (Wikipedia) (standard reference, not scraped)
Quotient space (topology) (Wikipedia) (standard reference, not scraped)

The cylinder and the Mobius band as quotients of the square by (0,y)∼(1,y)(0,y) \sim (1,y)(0,y)∼(1,y) and by (0,y)∼(1,1−y)(0,y) \sim (1, 1-y)(0,y)∼(1,1−y), both by a closed quotient map