Theorem 1.10: Borsuk–Ulam theorem for $S^2$

Proved

Hatcher.borsuk_ulam_sphere

by korbonits · Sep 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologycovering-spacesfundamental-grouphatcher

Let $S^2=\{x\in\mathbb{R}^3:\ |x|=1\}$ be the unit sphere. Theorem 1.10. For every continuous map $f:S^2\to\mathbb{R}^2$ there exists a pair of antipodal points $x$ and $-x$ in $S^2$ with

f(x)=f(-x) .

Hatcher proves it with the techniques used for $\pi_1(S^1)$ : if $f(x)\neq f(-x)$ everywhere, the map $g(x)=\big(f(x)-f(-x)\big)/|f(x)-f(-x)|$ restricted to the equator is a loop in $S^1$ whose lift to $\mathbb{R}$ changes by an odd integer over half a turn, so it is not null-homotopic; yet it extends over a hemisphere, so it is.

Formalization Note $S^2$ is Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1 with the subspace topology, and $-x$ is the antipodal point given by Mathlib's negation on spheres centred at the origin. The target $\mathbb{R}^2$ is EuclideanSpace ℝ (Fin 2).

Preamble

import Definitions.Def_Hatcher_Circle
import Mathlib

open unitInterval Hatcher

Formal statement

namespace Hatcher
theorem borsuk_ulam_sphere
    (f : C(Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1, EuclideanSpace ℝ (Fin 2))) :
    ∃ x, f x = f (-x) := by sorry
end Hatcher

Source

A. Hatcher, Algebraic Topology, Cambridge University Press 2002, https://pi.math.cornell.edu/~hatcher/AT/AT.pdf, Section 1.1, p. 32, Theorem 1.10

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Declaration borsuk_ulam_sphere.

Let $\mathbb{R}^3$ denote the space of real triples $y = (y_0, y_1, y_2)$ indexed by $\{0,1,2\}$ , and $\mathbb{R}^2$ the space of real pairs $(z_0, z_1)$ indexed by $\{0,1\}$ , each carried with the Euclidean ( $\ell^2$ ) norm

\|y\| = \sqrt{y_0^2 + y_1^2 + y_2^2}, \qquad \|z\| = \sqrt{z_0^2 + z_1^2},

and the metric $\operatorname{dist}(y, y') = \|y - y'\|$ it induces (in the source these are EuclideanSpace ℝ (Fin 3) and EuclideanSpace ℝ (Fin 2), i.e. the $L^2$ product PiLp 2 of copies of $\mathbb{R}$ ; the topology is the metric topology of this norm).

Let $S$ be the sphere of radius exactly $1$ centred at the origin $0 \in \mathbb{R}^3$ , namely the set

S = \{\, y \in \mathbb{R}^3 \;:\; \operatorname{dist}(y, 0) = 1 \,\} = \{\, y \in \mathbb{R}^3 \;:\; \|y\| = 1 \,\},

regarded as a topological space with the subspace topology inherited from $\mathbb{R}^3$ . (Membership is the equation $\operatorname{dist}(y,0) = 1$ with equality, not an inequality; the radius is the real number $1$ .)

On $S$ there is a negation operation $x \mapsto -x$ : for a point $x \in S$ , the point $-x$ is the coordinatewise negation $(-x_0, -x_1, -x_2)$ of $x$ taken in $\mathbb{R}^3$ , together with the (automatic) fact that it again lies on $S$ because $\|-x\| = \|x\| = 1$ . This is the antipodal map; it comes from the general construction that equips any sphere centred at $0$ in a seminormed group with negation inherited from the ambient space, and it satisfies $-(-x) = x$ .

The declaration asserts the following. For every function $f : S \to \mathbb{R}^2$ that is continuous (with respect to the subspace topology on $S$ and the Euclidean topology on $\mathbb{R}^2$ ) — this is the only hypothesis on $f$ ; no further structure (oddness, evenness, smoothness, injectivity, etc.) is assumed — there exists a point $x \in S$ such that

f(x) = f(-x),

where equality is equality in $\mathbb{R}^2$ , i.e. both coordinates agree: $f(x)_0 = f(-x)_0$ and $f(x)_1 = f(-x)_1$ .

Quantifier structure and edge cases, made explicit:

The point $x$ is existentially quantified after $f$ : it may depend on $f$ . The claim is plain existence ( $\exists$ ), not unique existence; nothing is said about how many such $x$ there are or where they lie.
The domain is fixed to the sphere of radius $1$ in $3$ real dimensions, and the target is fixed to $2$ real dimensions; there is no parameter $n$ in this statement.
The set $S$ is nonempty (e.g. $(1,0,0) \in S$ ), so the existential is not over an empty set. The statement does not require $x \neq -x$ ; on this particular $S$ no point satisfies $x = -x$ (that would force $x = 0$ , whose norm is $0 \neq 1$ ), but the declaration neither states nor uses this.
The continuity hypothesis is satisfiable (e.g. by constant maps), so the statement is not vacuous.
No custom definitions from the accompanying bundle are used by this declaration; every notion above is the standard Mathlib one, unfolded as described.

Human review

Endorsed by Shuze Chen · Sep 5, 2026
Endorsed by korbonits · Sep 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 1.10: Borsuk–Ulam theorem for S2S^2S2

Theorem 1.10: Borsuk–Ulam theorem for $S^2$