isOpen_coverU
plain-language theorem explainer
The northern chart on the n-sphere (sphere minus the south pole) is an open set. Anyone running Mayer–Vietoris on the two-punctured-sphere cover cites this. The proof is a one-line appeal to openness of singleton complements in a T1 space.
Claim. For every $n \in \mathbb{N}$, the set $U_n := S^n \setminus \{\text{south pole}\}$ is open in $S^n$.
background
The module builds singular homology of spheres via a standard two-set open cover. Write $S^n$ for the unit sphere in the ambient Euclidean space of the module, with distinguished north and south poles. The northern chart coverU n is defined as the complement of the south pole; the southern chart is the complement of the north pole.
These two sets form the classical cover used to run Mayer–Vietoris: their union is the whole sphere and their intersection deformation-retracts onto the equatorial $S^{n-1}$. Openness of each chart is the first topological hypothesis every connecting homomorphism and exactness statement needs.
Upstream, coverU is literally {southP n}ᶜ. No deeper sphere geometry is required for openness itself.
proof idea
One-line wrapper. Because coverU n is defined as the complement of a singleton, Mathlib’s isOpen_compl_singleton applies directly and yields IsOpen (coverU n).
why it matters
This lemma is the openness half of the two-chart cover that powers the whole sphere-homology package in the module. Downstream it is fed into:
suspensionIso, the Mayer–Vietoris connecting map that realises $H_{k+2}(S^{n+1}) \cong H_{k+1}(S^n)$;sphere_homology_vanish, Stage D vanishing $H_k(S^n)=0$ for $1\le k\ne n$;h1_s1_ne_zero, the base non-vanishing $H_1(S^1)\ne 0$ that seeds the inductive ladder.
In the Recognition foundation this supplies the topological backbone for dimension and octave arguments that later meet the forcing chain (T7 eight-tick period, T8 $D=3$). Without open charts the connecting maps are not even defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.