mem_inter_iff
plain-language theorem explainer
A point of the unit n-sphere lies in the intersection of the two standard open charts (sphere minus south pole and sphere minus north pole) if and only if it is neither pole. Anyone building stereographic charts, arc complements, or Mayer–Vietoris arguments on the doubly punctured sphere cites this. The proof is a two-line constructor that unpacks the set-complement definitions of the charts.
Claim. For every $n\in\mathbb{N}$ and every point $x$ of the unit $n$-sphere $S^n\subset\mathbb{R}^{n+1}$, one has $x\in U\cap V$ if and only if $x\neq S$ and $x\neq N$, where $U=S^n\setminus\{S\}$ is the sphere minus the south pole, $V=S^n\setminus\{N\}$ is the sphere minus the north pole, and $N$, $S$ are the north and south poles.
background
The ambient space is the unit sphere $\mathrm{Sph}(n)$ in Euclidean space $\mathbb{R}^{n+1}$ (as a topological space). The north pole $N$ is the last standard basis vector on the sphere; the south pole is $S=-N$.
The two standard open covers are defined by deleting one pole each: $\mathrm{coverU}(n)=S^n\setminus{S}$ and $\mathrm{coverV}(n)=S^n\setminus{N}$. Their intersection is the doubly punctured sphere, the natural domain for stereographic projection that sends $S$ to the origin of the equatorial hyperplane.
This module develops the singular-sphere geometry used later for arc complements and linking-vanishing statements in high dimension. The lemma is pure set algebra on those two chart definitions.
proof idea
Term-mode proof by constructor on the biconditional. Left-to-right: membership in both complements is exactly the pair of inequalities $x\neq S$ and $x\neq N$. Right-to-left: the same pair rebuilds membership in each complement. No external lemmas are needed; the argument is definitional unfolding of $\mathrm{coverU}$ and $\mathrm{coverV}$ as set complements.
why it matters
The doubly punctured sphere is the source of the stereographic homeomorphism interHomeoPunctured onto the punctured hyperplane, and this membership criterion is the gate for that construction. Downstream, it feeds eastP_mem_inter and westP_mem_inter (placing the equatorial poles in the intersection), the clopen arc decomposition isClopen_arcA, and the two-arc intersection identity range_arcPlus_inter_arcMinus.
Those facts support the abstract two-arc Mayer–Vietoris theorem isZero_h1_unionCompl (vanishing of $H_1$ on the complement of a union of closed arcs) and arc-segment intersection control in ArcComplementAcyclic. In the Recognition chain this geometry underwrites high-dimensional linking vanishing used when closing topological gaps between the forcing steps and recognition composition. It is local foundation, not a T0–T8 step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.