LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

A local homeomorphism from a nonempty compact space to a connected Hausdorff space is surjective with finite fibres

Statement

Let $f : X \to Y$ be a local homeomorphism. If $X$ is nonempty and compact and $Y$ is connected and Hausdorff, then $f$ is surjective and every fibre $f^{- 1} (y)$ is a nonempty finite discrete subspace of $X$ .

Facts & Assumptions

Given: A local homeomorphism $f : X \to Y$ with $X$ nonempty compact and $Y$ connected Hausdorff.

[F1]

Every point of the domain of a local homeomorphism has an open neighbourhood mapped homeomorphically onto an open subset of the target (Local homeomorphisms).

[F2]

A continuous image of a compact space is compact (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).

[F3]

Every compact subset of a Hausdorff space is closed (In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones).

[F4]

A closed subspace of a compact space is compact (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact).

[F5]

A space is compact when every open cover has a finite subcover (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[F6]

A connected space has no partition into two nonempty clopen subsets (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).

[F7]

Every singleton in a Hausdorff space is closed (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).

Proof

technique · direct

1.1

For every $x \in X$ , [F1] gives an open neighbourhood whose image is open. The union of these images is $f [X]$ , so $f [X]$ is open in $Y$ ; it is nonempty because $X$ is nonempty.

F1given

1.2

By [F2], $f [X]$ is compact, and by [F3] it is closed in the Hausdorff space $Y$ .

F2F3

1.3

Fix $y \in Y$ . The fibre $K = f^{- 1} (y)$ is closed because $f$ is continuous and ${y}$ is closed by [F7]. It is discrete: for each $x \in K$ , a local-homeomorphism chart $U_{x}$ is injective, hence $U_{x} \cap K = {x}$ , so every singleton is open in the subspace $K$ .

F1F7

2.1

The nonempty subset $f [X]$ is both open and closed. By connectedness in [F6], it must equal $Y$ , so $f$ is surjective.

step 1.1step 1.2F6

2.2

By [F4], the closed subspace $K$ of compact $X$ is compact.

step 1.3F4

3.1

The open singleton family ${{x} : x \in K}$ covers the discrete space $K$ . Compactness and [F5] give a finite subcover, so $K$ is finite. It is nonempty by surjectivity from step 2.1.

step 2.1step 1.3step 2.2F5∎

Depends on

Used by

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

Dependency tree · two levels

32 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

J. Peter May, A Concise Course in Algebraic Topology, Chapter 3, Problem 4 (standard reference, not scraped)