Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16
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.

The Hawaiian earring is locally path-connected but has no universal cover

Example

The Hawaiian earring is locally path-connected but is not semilocally simply connected at its wedge point. Consequently it has no universal cover.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

The loop t[t] in R/Z is not nullhomotopic. (The projected unit interval is not nullhomotopic in R/Z).

[F2]

If a space admits a universal covering, then it is semilocally simply connected. No local path-connectedness hypothesis is required. (A space admitting a universal covering is semilocally simply connected).

[F3]

A space X is semilocally simply connected at xX when there is a neighbourhood U of x and a basepoint-preserving inclusion (U,x)(X,x) whose induced map on fundamental groups is trivial (def-neighbourhood-top, def-induced-homomorphism-on-fundamental-groups, def-based-loops-and-fundamental-group). It is semilocally simply connected when this holds at every point. The neighbourhood need not itself be simply connected. (Semilocally simply connected spaces with explicit basepoint convention).

[F4]

The quotient topology. Let (X,T) be a topological space (def-topological-space), let Y be a set and let q:XY be a surjection (def-injection-surjection-bijection). The quotient topology on Y induced by q is the final topology of the one-element family (q) (def-initial-and-final-topology): Tq  :=  {VY:q1[V]T}. That this is a topology is discharged in def-initial-and-final-topology, where every final topology is verified to satisfy (T1), (T2) and (T3). Dually, CY is closed in Tq exactly when q1[C] is closed in X, because q1[YV]=Xq1[V]. (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection).

Verification

technique · direct
1.1

Model the earring as countably many copies of R/Z with diameters tending to zero and all zero classes identified, using the standard shrinking-wedge metric.

givenF1
2.1

Away from the wedge point, sufficiently short open arcs are path-connected neighbourhoods.

step 1.1F3F2
3.1

At the wedge point, every open neighbourhood contains a smaller metric ball whose intersection with each circle is an arc through the wedge point and which contains every sufficiently small circle, so that ball is path-connected.

step 2.1F3F2F4
4.1

Retraction to one such small circle and the essential unit loop show its inclusion carries a nontrivial loop, so semilocal simple connectedness fails at the wedge point.

step 3.1F1F2F3
5.1

The necessity theorem then rules out a universal cover.

step 4.1F2
6.1

The preceding construction and implications establish the assertion.

step 5.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 44 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources