Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

A local homeomorphism from a nonempty compact Hausdorff space to a connected Hausdorff space is a finite-sheeted covering

Statement

Let f:XY be a local homeomorphism. If X is nonempty, compact, and Hausdorff and Y is connected and Hausdorff, then f is a finite-sheeted covering map.

Facts & Assumptions

Given: A local homeomorphism f:XY satisfying the hypotheses in the Statement, and a point yY.

[L1]

Under these hypotheses, f is surjective and the fibre over every point is finite and nonempty (A local homeomorphism from a nonempty compact space to a connected Hausdorff space is surjective with finite fibres).

[F2]

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

[F6]

A covering map is a continuous surjection for which every target point has an open neighbourhood whose full preimage is a disjoint union of open sheets mapped homeomorphically onto that neighbourhood (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

Proof

technique · direct
1.1

List the finite fibre as f1(y)={x1,,xm} with m1 by [L1]. Using [F1] finitely many times and [F2] for the finite selections, choose pairwise disjoint open neighbourhoods Ni of the xi. Intersect each Ni with a local-homeomorphism chart at xi; its image is still an open neighbourhood of y. Let W be the finite intersection of these images, and replace each chart by its inverse image of W. We obtain pairwise disjoint open sets Ui with fUi:UiW a homeomorphism.

L1F1F2
2.1

The set K=XiUi is closed and therefore compact by [F3]. Its image f[K] is compact by [F4] and closed in Y by [F5]. No point of the fibre over y lies in K, so yf[K]. Hence V:=Wf[K] is an open neighbourhood of y.

step 1.1F3F4F5
3.1

Put Vi=Uif1(V). Each Vi is open and fVi:ViV is a homeomorphism. If xf1(V) then xK, so x lies in exactly one Ui and hence in exactly one Vi. Thus f1(V) is the disjoint union of the finitely many Vi. Since y was arbitrary and f is surjective by [L1], [F6] makes f a finite-sheeted covering.

step 1.1step 2.1L1F6

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

35 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