$\mathbb R^m\setminus\{0\}$ is simply connected for $m\ge3$

Proved

CauchyRiemannIndex.simplyConnectedSpace_nonzero_of_three_le_card

by Mazecto · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologyfundamental-grouphomotopy

Let $\iota$ be a finite set with at least three elements. Then the punctured space

\mathbb R^\iota\setminus\{0\}

is simply connected: it is nonempty, path-connected, and every loop in it is null-homotopic relative to its base point.

This is the case $m\ge3$ of the classical computation of the fundamental group of $\mathbb R^m\setminus\{0\}$ , stated for coordinate spaces $\mathbb R^\iota$ indexed by an arbitrary finite type so that it applies directly to spaces such as $\mathbb R^{2n}$ indexed by Fin n ⊕ Fin n.

Formalization Note. $\mathbb R^\iota$ is the function space ι → ℝ with its product topology, for [Fintype ι] with 3 ≤ Fintype.card ι; the punctured space is the subtype {y : ι → ℝ // y ≠ 0} with the subspace topology, and simple connectivity is Mathlib's SimplyConnectedSpace.

Preamble

import Definitions.Def_CauchyRiemannIndex_Setting
import Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Formal statement

namespace CauchyRiemannIndex

/-- If `ι` has at least three elements, the punctured space `ℝ^ι ∖ {0}` is simply connected. -/
theorem simplyConnectedSpace_nonzero_of_three_le_card {ι : Type*} [Fintype ι]
    (hι : 3 ≤ Fintype.card ι) : SimplyConnectedSpace {y : ι → ℝ // y ≠ 0} := by sorry

end CauchyRiemannIndex

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 3, §3.4, p. 62 (auxiliary fact for Theorem 3.34); A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Proposition 1.14 (

\pi_1(S^n)=0

for

n\ge2

)

View graph

Rm∖{0}\mathbb R^m\setminus\{0\}Rm∖{0} is simply connected for m≥3m\ge3m≥3

$\mathbb R^m\setminus\{0\}$ is simply connected for $m\ge3$