ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-31

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 cylinder is the preimage of a circle under a projection

Example

Let $π : R^{3} \to R^{2}$ be the projection $π (x, y, z) = (x, y)$ , and let $S^{1} = {(u, v) : u^{2} + v^{2} = 1}$ . Then

$π^{- 1} (S^{1}) = {(x, y, z) : x^{2} + y^{2} = 1} = S^{1} \times R,$

the standard circular cylinder, is an embedded submanifold of $R^{3}$ .

Facts & Assumptions

Given: The projection $π$ and the function $g (u, v) = u^{2} + v^{2}$ .

[L1]

The preimage of an embedded submanifold under a submersion is an embedded submanifold (The preimage theorem for submanifolds under submersions).

[L2]

A nonempty regular level set is an embedded submanifold (A regular level set is an embedded submanifold).

[L3]

The derivative of a square is $2 u$ , and derivative algebra handles sums (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

Verification

technique · direct

1.1L2L3given

The map $π$ is a submersion because its Jacobian is $[\begin{array}{ccc} 1 & 0 & 0 \\ 0 & 1 & 0 \end{array}]$ . For $g (u, v) = u^{2} + v^{2}$ , [L3] gives $D g_{(u, v)} (a, b) = 2 u a + 2 v b$ , which is surjective whenever $u^{2} + v^{2} = 1$ . The fibre is nonempty because $(1, 0) \in g^{- 1} (1)$ . Hence $S^{1} = g^{- 1} (1)$ is an embedded submanifold by [L2].

2.1L1step 1.1

Applying [L1] to the submersion $π$ and the embedded circle $S^{1}$ gives that $π^{- 1} (S^{1})$ is an embedded submanifold of $R^{3}$ .

3.1step 2.1∎

The displayed equation identifies this preimage with the usual cylinder.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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

John M. Lee, Introduction to Smooth Manifolds, Level Sets (standard reference, not scraped)