TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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 proper Euclidean local diffeomorphism has finite diffeomorphic sheets near every target point

Statement

Let $n \geq 1$ , let $U, V \subseteq R^{n}$ be nonempty open sets, let $V$ be connected, and let $f : U \to V$ be a proper $C^{1}$ map such that $D f (x)$ is invertible for every $x \in U$ . Then $f$ is surjective, every fibre is finite, and every $y \in V$ has an open neighbourhood whose preimage is a finite disjoint union of open sets, each carried $C^{1}$ -diffeomorphically onto that neighbourhood by $f$ .

Facts & Assumptions

Given: The hypotheses in the Statement. We use intrinsic compactness of subspaces (A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it), compact Euclidean closed balls (For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact), closedness of Euclidean compact sets (A compact subset of a metric space is closed and bounded), local inverses (The Euclidean inverse function theorem), and connectedness as the absence of a nontrivial clopen decomposition (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets, Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

[L1]

A continuous map $f : U \to V$ is proper when $f^{- 1} [K]$ is compact in $U$ for every compact subset $K$ of $V$ (Proper maps between Euclidean open sets).

[L2]

A $C^{1}$ map with everywhere-invertible derivative maps every open subset of its domain to an open subset of $R^{n}$ (A $C^{1}$ map with everywhere-invertible derivative is open).

[L3]

If $K$ is a compact subset of a metric space $X$ and $f : X \to Y$ is continuous into a metric space $Y$ , then $f [K]$ is compact in $Y$ (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

[L4]

A closed subset $F$ of a compact metric space $X$ is compact (A closed subset of a compact metric space is compact).

Proof

technique · direct

1.1L1L3L4given

The map $f$ is closed. Indeed, let $A \subseteq U$ be closed and let $y$ lie in the closure of $f [A]$ . Choose a compact closed target ball $K$ about $y$ contained in $V$ . By [L1], $f^{- 1} [K]$ is compact; $A \cap f^{- 1} [K]$ is compact by [L4], and its image is compact by [L3], hence closed in $V$ . Every sufficiently small neighbourhood of $y$ meets that image, so $y \in f [A]$ .

2.1step 1.1L1L2given

By [L2], $f [U]$ is open, and by step 1.1 it is closed. It is nonempty, so connectedness of $V$ gives $f [U] = V$ . For $y \in V$ , [L1] makes $f^{- 1} (y)$ compact. Local injectivity makes this fibre discrete, and its cover by neighbourhoods meeting the fibre in one point has a finite subcover; hence the fibre is nonempty and finite.

3.1step 1.1step 2.1givenchoose∎

Write $f^{- 1} (y) = {x_{1}, \dots, x_{s}}$ . Choose pairwise disjoint open local-inverse neighbourhoods $O_{i}$ of the $x_{i}$ , with open images $W_{i}$ . The closed set $U ∖ ⋃_{i} O_{i}$ has closed image by step 1.1 and that image omits $y$ . Therefore $W : = (⋂_{i} W_{i}) ∖ f [U ∖ ⋃_{i} O_{i}]$ is an open neighbourhood of $y$ . Its preimage is the disjoint union of $O_{i} \cap f^{- 1} [W]$ , and each restriction is a $C^{1}$ diffeomorphism onto $W$ .

Remarks

The neighbourhood property just proved is the one named by Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings ↗. The simply-connected one-sheet consequence is A connected covering of a locally path-connected simply connected space is one-sheeted and trivial ↗. Neither later result is used above.

Depends on

Used by

A proper Euclidean local diffeomorphism over a connected target has constant finite fibre cardinality Corollary

Dependency tree · two levels

46 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. M. Lee, Introduction to Smooth Manifolds, Proposition 2.19 (standard reference, not scraped)