Alphabeta Math
LemmaStatement: Literature-sourcedProof: 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.

Loops over a two-set path-connected open cover factor through the covering sets

Statement

Let X=U∪V, where U and V are open path-connected subsets of X, let U∩V be path-connected, and fix x0∈U∩V. If jU:U↪X and jV:V↪X are the inclusions, then every element of π1(X,x0) is a finite product of elements in the images of

(jU)∗:π1(U,x0)→π1(X,x0),(jV)∗:π1(V,x0)→π1(X,x0).

Equivalently, these two images generate π1(X,x0) (Based loops and the fundamental group, The homomorphism on fundamental groups induced by a pointed continuous map).

Facts & Assumptions

Given: The cover, basepoint, and inclusion maps in the Statement, and a based loop α:I→X at x0.

[F1]

If an open cover of a compact metric space has Lebesgue number δ>0, every nonempty subset of diameter less than δ lies in one cover member (Every open cover of a compact metric space has a Lebesgue number: a δ>0 such that every nonempty subset of diameter less than δ lies inside a single member of the cover).

[F2]

A space is path-connected when every pair of its points is joined by a path in that space (Paths, path-connected spaces and path components).

[F3]

Loop concatenation is well defined on path-homotopy classes and makes π1(X,x0) a group, with constant-loop identity and path-reversal inverses (Loop classes form the group π1(X,x0) under concatenation).

[F4]

A natural-number-indexed finite family of nonempty sets has a choice function, without any choice axiom (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

[F7]

For every real η>0 there is a natural q≥1 with 1/q<η (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε).

Proof

technique · direct
1.1F1F5F6F7F8

By [F5], α−1(U) and α−1(V) form an open cover of the compact metric interval I. Choose a Lebesgue number δ>0 by [F1], then choose q≥1 with 1/q<δ by [F7] and use the subdivision ti=i/q. Each restricted path αi:=α∣[ti−1,ti], reparametrized to I, is continuous by [F8] and lies wholly in U or wholly in V; assign it to U if its image lies in U, and to V otherwise. Merge adjacent pieces assigned to the same set. After merging, every interior subdivision value α(ti) lies in U∩V; the construction also admits the constant loop and the case of one retained piece.

2.1step 1.1F2F4choose

Put λ0=λm=cx0. For each remaining interior vertex, [F2] makes the family of paths in U∩V from x0 to α(ti) nonempty, so [F4] supplies paths λi for the finitely many vertices. If αi lies in Ai∈{U,V}, then βi:=λi−1∗αi∗λˉi is a based loop in Ai.

3.1step 2.1F3algebra∎

In the product [β1]⋯[βm], every adjacent pair λˉi∗λi cancels up to endpoint-fixed path homotopy, and the outside connectors are constant. Thus [F3] gives [α]=(jA1)∗[β1]⋯(jAm)∗[βm]. For m=1 this is the single factor [α], and for a constant loop it is the identity, so every loop class has the asserted factorization.

Depends on

Used by

Dependency tree · two levels

67 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