TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-24

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.

$R^{2}$ is not homeomorphic to $R^{n}$ for $n \neq 2$

Statement

For every natural number $n \neq 2$ , there is no homeomorphism $R^{2} \to R^{n}$ .

Facts & Assumptions

Given: A natural number $n \neq 2$ .

[L1]

At the standard basepoint, the punctured plane has fundamental group isomorphic to $Z$ ; if the given $n \geq 3$ , the punctured space $R^{n} ∖ {0}$ is simply connected (The punctured plane has fundamental group $Z$ , while punctured $R^{n}$ is simply connected for $n \geq 3$ ).

[L2]

For every $n \geq 2$ , there is no homeomorphism $R \to R^{n}$ ( $R$ is not homeomorphic to $R^{n}$ for any $n \geq 2$ ).

[F1]

A homeomorphism is a continuous bijection with continuous inverse (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological, Injection, surjection, bijection).

[L3]

Pointed continuous maps induce homomorphisms on fundamental groups, functorially; in particular a pointed homeomorphism induces an isomorphism (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

[L4]

The space $R^{0}$ has exactly one element, while for $m \geq 1$ the standard vector $e_{0} \in R^{m}$ is nonzero (The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ ).

[L5]

A map into $R^{m}$ is continuous exactly when its component functions are continuous; sums and scalar multiples of continuous Euclidean-valued maps are continuous (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).

Proof

technique · cases

1.1

If $n = 0$ , then $R^{0}$ is a singleton by [L4], while $0$ and $e_{0}$ are distinct points of $R^{2}$ ; hence no bijection, and therefore no homeomorphism, exists.

L4F1assume-case zero

1.2

If $n = 1$ , a homeomorphism $R^{2} \to R$ would have an inverse homeomorphism $R \to R^{2}$ , contrary to [L2].

L2F1assume-case one

1.3

It remains to treat $n \geq 3$ . Suppose $h : R^{2} \to R^{n}$ is a homeomorphism. Translating the target gives a homeomorphism $h_{0} (x) = h (x) - h (0)$ with $h_{0} (0) = 0$ ; its value $y = h_{0} (e_{0})$ is nonzero because $h_{0}$ is injective. Choose $j < n$ with $y_{j} \neq 0$ .

givenF1L4L5assume-case high

2.1

Let $P$ permute coordinate $j$ into coordinate $0$ , put $u = P (y)$ , and define $A : R^{n} \to R^{n}$ by $A (z)_{0} = z_{0} / u_{0}$ and $A (z)_{k} = z_{k} - (u_{k} / u_{0}) z_{0}$ for $1 \leq k < n$ . Its inverse is $A^{- 1} (w)_{0} = u_{0} w_{0}$ and $A^{- 1} (w)_{k} = w_{k} + u_{k} w_{0}$ , so [L5] makes $A$ a homeomorphism fixing $0$ and carrying $u$ to $e_{0}$ . Thus $g = A \circ P \circ h_{0}$ is a homeomorphism with $g (0) = 0$ and $g (e_{0}) = e_{0}$ .

step 1.3L5algebraconstruct

3.1

Restriction gives a pointed homeomorphism $(R^{2} ∖ {0}, e_{0}) \to (R^{n} ∖ {0}, e_{0})$ , so [L3] gives an isomorphism of their fundamental groups. This contradicts [L1], because the source is isomorphic to the nontrivial group $Z$ and the target is trivial. Hence no homeomorphism exists when $n \geq 3$ .

step 2.1L1L3

4.1

Since $n \neq 2$ , exactly one of $n = 0$ , $n = 1$ , or $n \geq 3$ holds, and steps 1.1, 1.2, and 3.1 exclude a homeomorphism in every case.

step 1.1step 1.2step 3.1cases-exhaustive∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

65 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

Allen Hatcher, Algebraic Topology, Corollary 1.16 (standard reference, not scraped)

R2R2 is not homeomorphic to RnRn for n≠2n=2