TheoremStatement: 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.

The regular locus of a $C^{1}$ Euclidean map is open

Statement

Let $n \geq 1$ . For a $C^{1}$ map $f : U \to R^{n}$ on an open $U \subseteq R^{n}$ , the regular locus $Reg (f)$ (The regular locus of a square-dimensional $C^{1}$ map) is open in $U$ . The empty regular locus is included.

Facts & Assumptions

Given: The map and domain in the Statement, with openness understood in the metric topology The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement.

[L1]

At a point $a$ where $D f (a)$ is invertible, there is $R > 0$ such that $D f (x)$ is invertible for every $x \in \overline{B} (a, R)$ (Newton maps are uniform contractions near a point with invertible derivative).

Proof

technique · direct

1.1

Fix $a \in Reg (f)$ . By [L1], some $R > 0$ has $B (a, R) \subseteq Reg (f)$ , so $a$ is an interior point of the regular locus.

L1given

2.1

Every point of the regular locus is interior by step 1.1; if the locus is empty, it is open by definition. Thus $Reg (f)$ is open.

step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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. Lebl, Basic Analysis II, §8.5 (standard reference, not scraped)

The regular locus of a C1C1 Euclidean map is open