isOpen_coverV
plain-language theorem explainer
The n-sphere with its north pole removed is an open subset of the sphere. Anyone running Mayer–Vietoris on the standard two-punctured cover cites this openness hypothesis. The proof is a one-line appeal to the fact that the complement of a singleton is open.
Claim. For every $n \in \mathbb{N}$, the set $S^n \setminus \{N\}$ is open in $S^n$, where $N$ denotes the north pole.
background
In this module the singular $n$-sphere $\mathrm{Sph},n$ is the unit sphere in the ambient Euclidean space used for Recognition foundation geometry. The north pole is a distinguished point on that sphere; the south pole is its antipode.
The set called the $V$-chart is defined as the complement of the singleton consisting of the north pole: $S^n \setminus {N}$. Its companion $U$-chart is the complement of the south pole. Together they form the classical two-set open cover of the sphere used for Mayer–Vietoris computations of singular homology.
Openness of each chart is the first structural hypothesis fed into the connecting homomorphism and the exactness statements that drive the suspension isomorphism and the vanishing theorems for $H_k(S^n)$.
proof idea
One-line wrapper. By definition the $V$-chart is exactly the complement of the singleton ${N}$. Mathlib’s isOpen_compl_singleton therefore applies directly and yields openness in the subspace topology on the sphere.
why it matters
Openness of the $V$-chart is a standing hypothesis of every Mayer–Vietoris map built from the two-punctured cover. Downstream it is passed into the suspension isomorphism $H_{k+2}(S^{n+1}) \cong H_{k+1}(S^n)$, into the Stage D vanishing theorem $H_k(S^n)=0$ for $1\le k\ne n$, and into the argument that $H_1(S^1)\ne 0$ (if that group vanished the connecting map would kill the point-difference class).
In the Recognition foundation stack these sphere-homology facts underwrite the geometric side of the forcing chain (dimension and octave structure). The lemma itself is pure topology; its value is that it discharges a recurring openness side-condition so the homology arguments stay clean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.