Proposition 1.14: $\pi_1(S^n)=0$ for $n\ge 2$

Declaration Hatcher.simplyConnected_sphere. The statement quantifies over a natural number $n \in \mathbb{N} = \{0, 1, 2, \dots\}$ together with one hypothesis $h_n : 2 \le n$ (non-strict; so $n = 2$ is included, and the cases $n = 0$ and $n = 1$ are excluded). Under that hypothesis it asserts that a certain topological space $S$ (described below) is simply connected in the sense defined by Mathlib. The theorem body is a sorry placeholder; no proof is supplied.

The space $S$. Let $E = \mathbb{R}^{n+1}$ denote Mathlib's EuclideanSpace ℝ (Fin (n+1)): the real vector space of functions $x : \{0, 1, \dots, n\} \to \mathbb{R}$ (i.e. $(n+1)$-tuples of reals, indices running over the finite type of $n+1$ elements) equipped with the $\ell^2$ (Euclidean) norm

and the metric topology it induces. Since $n \ge 2$, this is $\mathbb{R}^{m}$ with $m = n+1 \ge 3$. The space $S$ is Metric.sphere 0 1 in $E$, which by definition is the set

i.e. the unit sphere $S^n \subset \mathbb{R}^{n+1}$ centered at the origin with radius exactly $1$ (equality, not $\le$). Here $0$ is the zero vector of $E$. The set $S$ is regarded as a topological space in its own right via the subspace topology inherited from $E$ (Lean coerces the subset to a type whose points are pairs $(y, \text{proof that } \|y\| = 1)$, topologized as a subspace).

What "simply connected" means here. Mathlib's SimplyConnectedSpace S is a proposition defined as: there exists an equivalence of categories between the fundamental groupoid of $S$ and the discrete category on a single object (the one-object, one-morphism category Discrete Unit). Unfolding:

• The fundamental groupoid $\Pi(S)$ has as objects the points of $S$, and for $x, y \in S$ its morphisms $x \to y$ are the elements of $\operatorname{Path}(x,y)/\!\simeq$, i.e. homotopy classes of paths from $x$ to $y$. A path from $x$ to $y$ is a continuous map $\gamma : [0,1] \to S$ with $\gamma(0) = x$ and $\gamma(1) = y$; two such paths are homotopic when there is a homotopy $[0,1] \times [0,1] \to S$ between them that fixes the endpoints throughout (a homotopy relative to $\{0, 1\}$). Composition is concatenation of paths.
• The fundamental group $\pi_1(S, x)$ at a point $x \in S$ is, in Mathlib, the endomorphism (vertex) group of the object $x$ in $\Pi(S)$, i.e. the group of homotopy classes of loops $\gamma : [0,1] \to S$ with $\gamma(0) = \gamma(1) = x$ under concatenation.

Being equivalent to the one-object one-morphism category is, by Mathlib's own characterizations in the same file, equivalent to each of the following (all of which are therefore what the theorem asserts about $S$):

1. $S$ is nonempty, and for every pair of points $x, y \in S$ the set of homotopy classes of paths from $x$ to $y$ has exactly one element (it is Unique: nonempty and any two elements are equal).
2. $S$ is path-connected in Mathlib's sense — $S$ is nonempty and for all $x, y \in S$ there exists a continuous path in $S$ from $x$ to $y$ — and for all $x, y \in S$ any two paths from $x$ to $y$ are homotopic rel endpoints.
3. $S$ is path-connected (as in 2) and for every point $x \in S$ and every loop $\gamma$ in $S$ based at $x$, $\gamma$ is homotopic rel endpoints to the constant loop at $x$.

Consequently the statement includes, for every basepoint $x \in S$, that the fundamental group $\pi_1(S,x)$ is a subsingleton (has at most one element, hence is trivial), and that $S$ is path-connected; the nonemptiness of $S$ is part of the claim (not an extra hypothesis).

Custom definitions. The theorem sits inside the Hatcher namespace and imports the bundle's definitions file, but it does not use any of the bundle's custom definitions (basept, basept₂, inclHom, FreeProd, vanKampenHom, interHomLeft, interHomRight, vanKampenRelators, vanKampenNormal, loopIn, loopProd); every notion in the statement is from Mathlib.

Edge cases and scope. There are no implicit or typeclass arguments beyond $n$ and $h_n$; the metric, norm, and topology on $E$ and $S$ are the canonical Mathlib instances. The hypothesis $2 \le n$ is satisfiable (e.g. $n = 2$), so the theorem is not vacuous; it makes no claim about $n \in \{0, 1\}$ (the circle $S^1 \subset \mathbb{R}^2$ and $S^0 \subset \mathbb{R}^1$). The sphere is the one of radius $1$ centered at the origin only; nothing is asserted for other centers or radii. The statement is a single proposition (a typeclass-valued Prop), not a construction of a specific equivalence.