Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Antipodal complements cover Sn by simply connected sets with path-connected overlap for n≥2

Statement

Let n≥2 and write Sn⊆Rn+1 for the unit sphere (Euclidean spheres and closed balls as subspaces of Rn). For any coordinate unit vector ej, put

Uj=Sn∖{ej},Vj=Sn∖{−ej}.

Then Uj and Vj are open, simply connected subsets of Sn, they cover Sn, and their intersection is path-connected. More precisely, stereographic projection gives homeomorphisms Uj≅Rn, Vj≅Rn, and Uj∩Vj≅Rn∖{0}.

Facts & Assumptions

Given: A natural n≥2, a coordinate index j<n+1, the unit vector ej, and the unit sphere Sn⊆Rn+1.

[F1]

The unit sphere Sn is the set of z∈Rn+1 with ∥z∥2=1 (Euclidean spheres and closed balls as subspaces of Rn).

[F2]

Sums and products of continuous real maps are continuous, and a quotient is continuous wherever its denominator is nonzero (Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined).

[F3]

Continuity of maps into a finite-dimensional Euclidean space is equivalent to continuity of every coordinate map (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).

[F5]

Every nonempty convex subset of Rn is simply connected (Every nonempty convex subset of Rn is simply connected).

[F6]

For n≥2, Rn∖{0} is polygonally connected, hence path-connected (For n≥2, the punctured space Rn∖{0} is polygonally connected).

[F7]

Pointed homeomorphisms induce mutually inverse fundamental-group homomorphisms (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

[F8]

A space is simply connected when it is nonempty and path-connected and its fundamental group has one element at every basepoint (Simply connected topological spaces).

Proof

technique · direct
1.1F1algebra

Delete the j-th coordinate to identify ej⊥ with Rn, and write z=u+tej. Projection from ej is σ+(z)=u/(1−t) on Uj, with inverse τ+(y)=2y∥y∥22+1+∥y∥22−1∥y∥22+1ej. Projection from −ej is σ−(z)=u/(1+t) on Vj, with inverse τ−(y)=2y∥y∥22+1+1−∥y∥22∥y∥22+1ej. Since ∥y∥22≥0, the inverse denominator ∥y∥22+1 is positive. The sphere equation ∥u∥22+t2=1 and deletion of the relevant pole give 1−t≠0 on Uj and 1+t≠0 on Vj. The same equation shows that both inverse formulas land on Sn, and direct substitution gives σ±τ±=id⁡ and τ±σ±=id⁡.

2.1step 1.1F2F3F4

The coordinate t is continuous, so Uj={z∈Sn:t<1} and Vj={z∈Sn:t>−1} are open by [F4]. They cover the sphere because no point has both t=1 and t=−1. The formulas in step 1.1 are continuous by [F2] and [F3], so they are the asserted homeomorphisms. Moreover σ+ sends the deleted point −ej to 0, hence restricts to a homeomorphism Uj∩Vj≅Rn∖{0}.

3.1step 2.1F5F7F8

The space Rn is nonempty and convex, so [F5] makes it simply connected. Each homeomorphism in step 2.1 transports paths, and [F7] applied to it and its inverse transports the one-element fundamental group at every basepoint. Thus [F8] makes both Uj and Vj simply connected.

4.1step 2.1F6∎

By [F6] and the last homeomorphism in step 2.1, Uj∩Vj is path-connected. This proves every assertion.

Depends on

Used by

Dependency tree · two levels

62 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources