FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013)

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 25 definitions, 11 theorems, 19 propositions, 1 lemma, 5 corollaries, 8 examples and 1 convention.

Of the 70 statements checked against Lean, 0 are formalized somewhere and 70 are not.

Status	Statements	Share	What it means
not formalized	70	100%	A documented search found no Lean statement of it anywhere.
checked in total	70

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 5, FC08-C05-U001–FC08-C05-U070, exactly 70 unique contiguous rows retrieved from FC08 — John M. Lee, Introduction to Smooth Manifolds through agent-memory.
Search order followed the Sweep-II plan: project source first at A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean 4.33.0), current upstream Mathlib H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0, Lean 4.34.0-rc2), then targeted current/indexed/external Lean searches and local reference probes. No mathlib, project-existing, package-import, or reference-port C05 row survived strict whole-row checking.
C05 therefore has 0 promoted rows and 70 dated unmatched rows. This is not a failure to find nearby manifold machinery: it records a specific missing abstraction boundary. At P, Mathlib/Geometry/Manifold/SmoothEmbedding.lean says its IsSmoothEmbedding map predicate “will be useful to define embedded submanifolds”; no embedded-submanifold definition is present. IsManifold/InteriorBoundary.lean explicitly lists “boundary M is a submanifold … this requires a definition of submanifolds” as TODO. Current H still has no Submanifold, regular-value, or level-set manifold file/interface.
The same boundary controls the immersed rows. Immersion.lean and Submersion.lean define map predicates by local normal forms, not Lee’s finite-dimensional injective/surjective differential definitions. At P both files state the finite-dimensional equivalence as future work. H adds differential-immersion infrastructure and one implication toward injective mfderiv, but no complete equivalence to IsImmersion and no parallel differential-submersion package. Therefore C05’s image-of-immersion, immersed-submanifold, local-parametrization, level-set, and restriction theorems cannot be routed through those map predicates without an unproved bridge.
Several ingredients were checked and deliberately not promoted as whole rows: IsSmoothEmbedding.of_opens for open inclusions; Topology.isEmbedding_graph plus ContMDiff.prodMk for graph maps; proper-map/closed-embedding results; ContMDiff.subtypeVal_comp_iff for open subtypes; smooth sphere APIs; TangentSpace/mfderiv; and generic models with corners. Each owns only a proper subset or specialization of the corresponding C05 statement and does not construct the required submanifold topology/smooth structure.
The level-set block U017–U027 was searched separately. P/H have no manifold RegularPoint, RegularValue, RegularLevelSet, or regular-value/submersion-level-set theorem. Thus even where generic preimage/singleton or linear rank-nullity primitives exist, there is no checked owner for Lee’s manifold-level definitions and codimension/proper-embedded conclusions.
The boundary block U055–U070 was also searched separately. P/H expose IsBoundaryPoint, boundary, interior, local-diffeomorphism boundary preservation, interval/half-space models, and related chart APIs, but no inward/outward tangent-vector predicate, boundary defining function, regular domain, half-slice criterion, or general submanifold-with-boundary package.
U063 has a separate canonical-source defect: its Sweep-I statement is truncated to Suppose M is a smooth manifold and f ∈ C^∞(M). with no conclusion. Sweep II leaves that canonical row unmatched rather than reconstructing a proposition from an external edition and thereby mutating Sweep-I content implicitly.
Project-first search found no C05 submanifold implementation. LeanCategories/ForMathlib/QuotientManifold.lean from the preceding covering audit is a specialized quotient-manifold construction, not a submanifold package and does not close any C05 row.
Targeted indexed GitHub searches for Lean formalizations of embedded/immersed submanifolds, regular level sets, and boundary defining functions returned no compatible general owner. A current TauCeti roadmap result independently describes embedded-submanifold infrastructure as absent from Mathlib, consistent with the checked source-tree evidence; this secondary evidence was not used in place of direct revision inspection.
N=2026-09-07 marks a dated unmatched decision after the prescribed search layers. Strict whole-row semantics apply uniformly.

Definition/convention — embedded submanifold of M is a subset S M that

FC08-C05-U001 · Ch. 5, § Embedded Submanifolds; source L2759 · not formalized

Suppose M is a smooth manifold with or without boundary. An embedded submanifold of M is a subset S M that is a manifold (without boundary) in the subspace topology, endowed with a smooth structure with respect to which the inclusion map $S \hookrightarrow M$ is a smooth embedding. Embedded submanifolds are also called regular submanifolds; the difference $\dim M - \dim S$ is the codimension of $S$ in $M$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has IsSmoothEmbedding, open-subtype manifolds, product/graph embedding ingredients, proper-map topology, and boundary/interior sets, but no EmbeddedSubmanifold object or theorem constructing/characterizing embedded submanifolds. SmoothEmbedding.lean explicitly says its map predicate is intended to support a future definition; InteriorBoundary.lean likewise lists “boundary M is a submanifold” as TODO. Thus the full source row has no owner. Strict bundle semantics reject a proper subset, isolated ingredient, unbridged equivalent notion, stronger-hypothesis specialization, or reconstruction of the substantive source theorem.

Definition/convention — regular submanifolds by some authors

FC08-C05-U002 · Ch. 5, § Embedded Submanifolds; source L2761 · not formalized

S ↪ M is a smooth embedding. Embedded submanifolds are also called regular submanifolds by some authors.

Definition/convention — codimension of S in M

FC08-C05-U003 · Ch. 5, § Embedded Submanifolds; source L2763 · not formalized

If S is an embedded submanifold of M; the difference dim M dim S is called the codimension of S in M , and the containing manifold M is called the ambient manifold for S. An embedded hypersurface is an embedded submanifold of codimension 1. The empty set is an embedded submanifold of any dimension.

Proposition 5.1

FC08-C05-U004 · Ch. 5, § Embedded Submanifolds; source L2767 · not formalized

Proposition 5.1 (Open Submanifolds). Suppose M is a smooth manifold. The embedded submanifolds of codimension 0 in M are exactly the open submanifolds.

Proposition 5.2

FC08-C05-U005 · Ch. 5, § Embedded Submanifolds; source L2773 · not formalized

Proposition 5.2 (Images of Embeddings as Submanifolds). Suppose M is a smooth manifold with $o r$ without boundary, N is $a$ smooth manifold, and $F \colon N \to M$ is a smooth embedding. Let $S = F ( N )$ . With the subspace topology, S is a topological manifold, and it has a unique smooth structure making it into an embedded submanifold of M with the property that F is a diffeomorphism onto its image.

Proposition 5.3

FC08-C05-U006 · Ch. 5, § Embedded Submanifolds; source L2788 · not formalized

Proposition 5.3 (Slices of Product Manifolds). Suppose M and N are smooth manifolds. For each $p \in N$ , the subset $M \times \{ p \}$ (called a slice of the product manifold) is an embedded submanifold of M N diffeomorphic to M .

Proposition 5.4

FC08-C05-U007 · Ch. 5, § Embedded Submanifolds; source L2792 · not formalized

Proposition 5.4 (Graphs as Submanifolds). Suppose M is a smooth m-manifold (without boundary), N is a smooth n-manifold with or without boundary, $U \subseteq M$ is open, and $f \colon U \to N$ is a smooth map. Let $\Gamma ( f ) \subseteq M \times N$ denote the graph of f : \[ \Gamma (f) = \left\{(x, y) \in M \times N: x \in U, y = f (x) \right\}. \] Then $\Gamma ( f )$ is an embedded m-dimensional submanifold of $M \times N$ (se even if it is known to be a surjective local diffeomorphism.

Definition/convention — properly embedded

FC08-C05-U008 · Ch. 5, § Embedded Submanifolds; source L2808 · not formalized

An embedded submanifold $S \subseteq M$ is properly embedded if the inclusion $S \hookrightarrow M$ is a proper map; merely being embedded is not always a strong enough condition.

Proposition 5.5

FC08-C05-U009 · Ch. 5, § Embedded Submanifolds; source L2810 · not formalized

Proposition 5.5. Suppose M is a smooth manifold with or without boundary and $S \subseteq M$ is an embedded submanifold. Then S is properly embedded if and only if it is a closed subset of M .

Corollary 5.6

FC08-C05-U010 · Ch. 5, § Embedded Submanifolds; source L2814 · not formalized

Corollary 5.6. Every compact embedded submanifold is properly embedded.

Proposition 5.7

FC08-C05-U011 · Ch. 5, § Embedded Submanifolds; source L2820 · after FC08-C05-U007 · not formalized

Proposition 5.7 (Global Graphs Are Properly Embedded). Suppose M is a smooth manifold, N is a smooth manifold with or without boundary, and $f \colon M \to N$ is a smooth map. With the smooth manifold structure of Proposition 5.4, .f / is properly embedded U by the connected component of U containing $q _ { \mathrm { : } }$ , we can assume that U is connected and still satisfies (4.8) and (4.9).

Definition/convention — k-dimensional slice

FC08-C05-U012 · Ch. 5, § Slice Charts for Embedded Submanifolds; source L2832 · not formalized

Somewhat more generally, if U is an open subset of $\mathbb { R } ^ { n }$ and $k \in \{ 0 , \ldots , n \}$ , a kdimensional slice of U (or simply a $_ { k - s l i c e ) }$ is any subset of the form \[ S = \left\{\left(x ^ {1}, \dots , x ^ {k}, x ^ {k + 1}, \dots , x ^ {n}\right) \in U: x ^ {k + 1} = c ^ {k + 1}, \dots , x ^ {n} = c ^ {n} \right\} \] for some constants $c ^ { k + 1 } , \ldots , c ^ { n }$ . (When $k = n$ , this just means $S = U . )$ Clearly, every k-slice is homeomorphic to an open subset of $\mathbb { R } ^ { \check { k } }$ . (Sometimes it is convenient to consider slices defined by setting some subset of the coordinates other than the last ones equal to constants. The meaning should e a version of the rank theorem for a map of constant rank whose domain is a smooth manifold with boundary.

Definition/convention — slice chart for S in M

FC08-C05-U013 · Ch. 5, § Slice Charts for Embedded Submanifolds; source L2840 · not formalized

Let M be a smooth n-manifold, and let $( U , \varphi )$ be a smooth chart on M . If S is a subset of U such that $\varphi ( S )$ is a k-slice of $\varphi ( U )$ , then we say that S is a kslice of U . (Although in general we allow our slices to be defined by arbitrary constants ${ \bar { c } } ^ { k + 1 } , \ldots , { \bar { c } } ^ { n }$ , it is sometimes useful to have slice coordinates for which the constants are all zero, which can easily be achieved by subtracting a constant from each coordinate function.) Given a subset $S \subseteq M$ and a nonnegative integer k, we say that S satisfies the local k-slice condition if each point of S is contained in the domain of a smooth chart $( U , \varphi )$ for M such that S U is a single k-slice in U . Any such chart is called a slice chart for S in M , and the corresponding coordinates $\left( x ^ { 1 } , \ldots , x ^ { n } \right)$ are called slice coordinates.

Theorem 5.8

FC08-C05-U014 · Ch. 5, § Slice Charts for Embedded Submanifolds; source L2842 · not formalized

Theorem 5.8 (Local Slice Criterion for Embedded Submanifolds). Let M be a smooth n-manifold. $I f S \subseteq M$ is an embedded k-dimensional submanifold, then S satisfies the local k-slice condition. Conversely, if $S \subseteq M$ is a subset that satisfies the local k-slice condition, then with the subspace topology, S is a topological manifold of dimension k, and it has a smooth structure making it into a k-dimensional embedded submanifold of M .

Example 5.9

FC08-C05-U015 · Ch. 5, § Slice Charts for Embedded Submanifolds; source L2884 · after FC08-C01-U008 · not formalized

(Spheres as submanifolds). For any $n \geq 0$, $\mathbb{S}^{n}$ is an embedded submanifold of $\mathbb{R}^{n+1}$, because it is locally the graph of a smooth function: the intersection of $\mathbb{S}^{n}$ with the open subset $\{x : x^{i} > 0\}$ is the graph of \[ x^{i} = f(x^{1},\dots,x^{i-1},x^{i+1},\dots,x^{n+1}), \] where $f \colon \mathbb{B}^{n} \to \mathbb{R}$ is $f(u) = \sqrt{1 - |u|^{2}}$, and its intersection with $\{x : x^{i} < 0\}$ is the graph of $-f$. Every point of $\mathbb{S}^{n}$ lies in one of these sets, so $\mathbb{S}^{n}$ satisfies the local $n$-slice condition; the induced smooth structure is the one defined in Chapter 1.

Theorem 5.11

FC08-C05-U016 · Ch. 5, § Slice Charts for Embedded Submanifolds; source L2897 · not formalized

Theorem 5.11. If M is a smooth n-manifold with boundary, then with the subspace topology, @M is a topological .n 1/-dimensional manifold (without boundary), and has a smooth structure such that it is a properly embedded submanifold of M . P

Definition/convention — zero set of clubsuit

FC08-C05-U017 · Ch. 5, § Level Sets; source L2905 · after FC08-C01-U044 · not formalized

In practice, embedded submanifolds are most often presented as solution sets of equations or systems of equations. Extending the terminology we introduced in Example 1.32, if $\Phi \colon M \to N$ is any map and c is any point of N , we call the set $\phi ^ { - 1 } ( c )$ a level set of ˚ (Fig. 5.4). (In the special case $\overset { \vartriangle } { \boldsymbol { N } } = \mathbb { R } ^ { k }$ and $c = 0$ , the level set $\Phi ^ { - 1 } ( 0 )$ is usually called the zero set of $\Phi$.)

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has the underlying set/function/differential primitives, but no named manifold interface for this source definition (level/zero sets, regular points/values/level sets, defining maps/functions, boundary defining functions, or regular sublevel sets) with the complete Lee semantics. Strict bundle semantics reject a proper subset, isolated ingredient, unbridged equivalent notion, stronger-hypothesis specialization, or reconstruction of the substantive source theorem.

Theorem 5.12

FC08-C05-U018 · Ch. 5, § Level Sets; source L2917 · not formalized

Theorem 5.12 (Constant-Rank Level Set Theorem). Let M and N be smooth manifolds, and let $\Phi \colon M \to N$ be a smooth map with constant rank r. Each level set of $\varPhi$ is a properly embedded submanifold of codimension l linear group $\mathrm { G L } ( n , \mathbb { R } )$ is the set of invertible $n \times n$ matrices with real entries.

Not formalized. none; no complete checked declaration under strict bundle semantics — The checked manifold library has no regular-value/level-set theorem or embedded-submanifold package. In addition, Lee’s submersion notion here is derivative-surjectivity, while pinned IsSubmersion is a local-normal-form predicate whose finite-dimensional equivalence is explicitly future work. Level-set and defining-map ingredients therefore do not close this row under strict semantics. Strict bundle semantics reject a proper subset, isolated ingredient, unbridged equivalent notion, stronger-hypothesis specialization, or reconstruction of the substantive source theorem.

Corollary 5.13

FC08-C05-U019 · Ch. 5, § Level Sets; source L2927 · not formalized

Corollary 5.13 (Submersion Level Set Theorem). If M and N are smooth manifolds and ˚ $M \to N$ is a smooth submersion, then each level set of ˚ is a properly embedded submanifold whose codimension is equal to the dimension of N .

Definition/convention — surjective linear map

FC08-C05-U020 · Ch. 5, § Level Sets; source L2931 · not formalized

This result should be compared to the corresponding result in linear algebra: if $L \colon \mathbb { R } ^ { m } \to \mathbb { R } ^ { r }$ is a surjective linear map, then the kernel of L is a linear subspace of codimension r by the rank-nullity law. The vector equation $L x = 0$ is equivalent to r linearly independent scalar equations, each of which can be thought of as cutting down one of the degrees of freedom in $\mathbb { R } ^ { m }$ , leaving a subspace of codimension r. In the context of smooth manifolds, the analogue of a surjective linear map is a smooth submersion, each of whose (local) component functions cuts down the dimension by one.

Definition/convention — regular level set

FC08-C05-U021 · Ch. 5, § Level Sets; source L2933 · after FC08-C05-U019, FC08-C04-U004 · not formalized

Corollary 5.13 can be strengthened considerably, because we need only check the submersion condition on the level set we are interested in. If $\phi \colon M \to N$ is a smooth map, a point $p \in M$ is said to be a regular point of ˚ if $d \Phi _ { p } \colon T _ { p } M \to$ $T _ { \Phi ( p ) } N$ is surjective; it is a critical point of ˚ otherwise. This means, in particular, that every point of M is critical if dim M < dim N , and every point is regular if and only if F is a submersion. Note that the set of regular points of $\varPhi$ is always an open subset of M by Proposition 4.1. A point $c \in N$ is said to be a regular value of ˚ if every point of the level set $\scriptstyle { \phi ^ { - 1 } ( c ) }$ is a regular point, and a critical value otherwise. In particular, if $\phi ^ { - 1 } ( c ) = \emptyset$ , then $c$ is a regular value. Finally, a level set ${ \phi } ^ { - 1 } ( c )$ is called a regular level set if c is a regular value of $\varPhi$ ; in other words, a regular level set is a level set consisting entirely of regular points of ˚ (points p such that $d \phi _ { p }$ is surjective).

Corollary 5.14

FC08-C05-U022 · Ch. 5, § Level Sets; source L2938 · not formalized

Corollary 5.14 (Regular Level Set Theorem). Every regular level set of a smooth map between smooth manifolds is a properly embedded submanifold whose codimension is equal to the dimension of the codomain.

Example 5.15

FC08-C05-U023 · Ch. 5, § Level Sets; source L2944 · not formalized

(Spheres). The sphere is a regular level set of the smooth function $f \colon \mathbb{R}^{n+1} \to \mathbb{R}$ given by $f(x) = |x|^{2}$, since \[ df_{x}(v) = 2\sum_{i} x^{i}v^{i} \] is surjective except at the origin; so $\mathbb{S}^{n}$ is an embedded submanifold of $\mathbb{R}^{n+1}$.

Proposition 5.16

FC08-C05-U024 · Ch. 5, § Level Sets; source L2948 · not formalized

Proposition 5.16. Let S be a subset of a smooth m-manifold M . Then S is an embedded k-submanifold of M if and only if every point of S has a neighborhood U in M such that $U \cap S$ is a level set of a smooth submersion $\phi \colon U \to { \overline { { \mathbb { R } } } } ^ { m - k }$ Proof. First suppose S is an embedded k-submanifold. If $\left( x ^ { 1 } , \ldots , x ^ { m } \right)$ are slice coordinates on a chart $U$, the last $m-k$ of them form such a submersion.

Definition/convention — defining map for S

FC08-C05-U025 · Ch. 5, § Level Sets; source L2955 · after FC08-C05-U023, FC08-C05-U024 · not formalized

If $S \subseteq M$ is an embedded submanifold, a smooth map $\Phi \colon M \to N$ for which $S$ is a regular level set is a defining map for $S$; when $N = \mathbb{R}^{m-k}$, so that $\Phi$ is vector-valued, it is called a defining function. Example 5.15 shows $f(x) = |x|^{2}$ is a defining function for the sphere. If $U \subseteq M$ is open and $\Phi \colon U \to N$ is smooth with $S \cap U$ a regular level set of $\Phi$, then $\Phi$ is a local defining map, or local defining function, for $S$. Proposition 5.16 says every embedded submanifold admits one in a neighborhood of each of its points.

Example 5.17

FC08-C05-U026 · Ch. 5, § Level Sets; source L2959 · after FC08-C04-U005 · not formalized

(Surfaces of Revolution). Let $H$ be the half-plane $\{(r,z) : r > 0\}$ and let $C \subseteq H$ be an embedded 1-dimensional submanifold. At any point $(x,y,z) \in S_{C}$ at least one component of $D\Phi(x,y,z)$ is nonzero, so $S_{C}$ is a regular level set of $\Phi$ and hence an embedded 2-dimensional submanifold of $\mathbb{R}^{3}$. For example, the torus of revolution of Example 4.2(d) is obtained from the circle $(r-2)^{2} + z^{2} = 1$, its generating curve, and is a regular level set of \[ \Phi(x,y,z) = \left(\sqrt{x^{2}+y^{2}} - 2\right)^{2} + z^{2}, \] which is smooth on $\mathbb{R}^{3}$ minus the $z$-axis.

Definition/convention — generating curve

FC08-C05-U027 · Ch. 5, § Level Sets; source L2965 · not formalized

The set $C$ is called the generating curve of the surface of revolution $S_{C}$. If $\varphi \colon U \to \mathbb{R}$ is any local defining function for $C$ in the half-plane $H$, a local defining function $\Phi$ for $S_{C}$ is \[ \Phi(x,y,z) = \varphi\!\left(\sqrt{x^{2}+y^{2}},\, z\right), \] defined on the open subset \[ \widetilde{U} = \left\{(x,y,z) : \left(\sqrt{x^{2}+y^{2}},\, z\right) \in U\right\} \subseteq \mathbb{R}^{3}. \]

Definition/convention — codimension of S in M to be dim M - dim S

FC08-C05-U028 · Ch. 5, § Immersed Submanifolds; source L2994 · not formalized

So as to have a convenient language for talking about examples like these, we introduce the following definition. Let M be a smooth manifold with or without boundary. An immersed submanifold of M is a subset $S \subseteq M$ endowed with a topology (not necessarily the subspace topology) with respect to which it is a topological manifold (without boundary), and a smooth structure with respect to which the inclusion map $S \hookrightarrow M$ is a smooth immersion. As for embedded submanifolds, we define the codimension of S in M to be dim $M - \dim S .$

Not formalized. none; no complete checked declaration under strict bundle semantics — There is no checked ImmersedSubmanifold object/package. Mathlib’s IsImmersion is a predicate on maps, not a topology/smooth-structure on an image subset, and at P its equivalence with Lee’s derivative-injective definition is future work. Generic embedding/graph/local-chart ingredients do not supply the image topology, uniqueness, local parametrization, or immersed-versus-embedded claims bundled in this row. Strict bundle semantics reject a proper subset, isolated ingredient, unbridged equivalent notion, stronger-hypothesis specialization, or reconstruction of the substantive source theorem.

Definition/convention — source terminology/construction

FC08-C05-U029 · Ch. 5, § Immersed Submanifolds; source L2996 · not formalized

Every embedded submanifold is also an immersed submanifold. Because immersed submanifolds are the more general of the two types of submanifolds, we adopt the convention that the term smooth submanifold without further qualification means an immersed one, which includes an embedded submanifold as a special case. Similarly, the term smooth hypersurface without qualification means an immersed submanifold of codimension 1.

Definition/convention — source terminology/construction

FC08-C05-U030 · Ch. 5, § Immersed Submanifolds; source L2998 · not formalized

You should be aware that there are variations in how smooth submanifolds are defined in the literature. Some authors reserve the unqualified term “submanifold” to mean what we call an embedded submanifold. If there is room for confusion, it is safest to specify explicitly which type of submanifold—embedded or immersed—is meant. Even though both terms “smooth submanifold” and “immersed submanifold” encompass embedded ones as well, when we are considering general submanifolds we sometimes use the phrase immersed or embedded submanifold as a reminder that the discussion applies equally to the embedded case. (Some

Definition/convention — immersed topological submanifold of M to be a subset S

FC08-C05-U031 · Ch. 5, § Immersed Submanifolds; source L3002 · not formalized

There are also various notions of submanifolds in the topological category. For example, if M is a topological manifold, one could define an immersed topological submanifold of M to be a subset $S \subseteq M$ endowed with a topology such that it is a topological manifold and such that the inclusion map is a topological immersion. It is an embedded topological submanifold if the inclusion is a topological embedding. To be entirely consistent with our convention of assuming by default only continuity rather than smoothness, we would have to distinguish the types of submanifolds we have defined in this chapter by calling them smooth embedded submanifolds and smooth immersed submanifolds, respectively; but since we have no reason to treat topological submanifolds in this book, for the sake of simplicity let us agree that the terms embedded submanifold and immersed submanifold always refer to the smooth kind.

Proposition 5.18

FC08-C05-U032 · Ch. 5, § Immersed Submanifolds; source L3006 · not formalized

Proposition 5.18 (Images of Immersions as Submanifolds). Suppose M is a smooth manifold with or without boundary, N is a smooth manifold, and F $N $ M is an injective smooth immersion. Let $S = F ( N )$ . Then S has a unique topology and smooth structure such that it is a smooth submanifold of M and such that $F \colon N S$ is a diffeomorphism onto its ima Fig.

Example 5.19

FC08-C05-U033 · Ch. 5, § Immersed Submanifolds; source L3018 · after FC08-C04-U019, FC08-C04-U020 · not formalized

Example 5.19 (The Figure-Eight and the Dense Curve on the Torus). Look back at the two examples we introduced in Chapter 4 of injective smooth immersions that are not embeddings: because the figure-eight of Example 4.19 and the dense curve of Example 4.20 are images of injective smooth immersions, they are immersed submanifolds when given appropriate topologies and smooth structures. They are not embedded submanifolds, because neither one has the subspace topology. In fact, their image sets cannot be made into embedded submanifolds even if we are allowed to change their topologies and smooth structures (see Problems 5-4 and 5-5).

Proposition 5.21

FC08-C05-U034 · Ch. 5, § Immersed Submanifolds; source L3026 · not formalized

Proposition 5.21. Suppose M is a smooth manifold with or without boundary, and $S \subseteq M$ is an immersed submanifold. If any of the following holds, then S is embedded. (a) S has codimension 0 in M . (b) The inclusion map S M is proper. (c) S is compact.

Proposition 5.22

FC08-C05-U035 · Ch. 5, § Immersed Submanifolds; source L3038 · not formalized

Proposition 5.22 (Immersed Submanifolds Are Locally Embedded). If M is a smooth manifold with or without boundary, and $S \subseteq M$ is an immersed submanifold, then for each $p \in S$ there exists a neighborhood U of p in S that is an embedded submanifold of M .

Definition/convention — smooth local parametrization

FC08-C05-U036 · Ch. 5, § Immersed Submanifolds; source L3047 · not formalized

Suppose S M is an immersed k-dimensional submanifold. A local parametrization of S is a continuous map $X \colon U \to M$ whose domain is an open subset $U \subseteq \mathbb { R } ^ { k }$ , whose image is an open subset of S, and which, considered as a map into S , is a homeomorphism onto its image. It is called a smooth local parametrization if it is a diffeomorphism onto its image (with respect to $S ^ { \prime } { \bf s }$ smooth manifold structure). If the image of X is all of S , it is called a global paramet smooth map between smooth manifolds is a properly embedded submanifold whose codimension is equal to the dimension of the codomain.

Proposition 5.23

FC08-C05-U037 · Ch. 5, § Immersed Submanifolds; source L3049 · not formalized

Proposition 5.23. Suppose M is a smooth manifold with or without boundary, $S \subseteq$ M is an immersed k-submanifold, $\iota \colon S \hookrightarrow M$ is the inclusion map, and U is an open subset of $\mathbb { R } ^ { k }$ . A map $X \colon U \to M$ is a smooth local parametrization of S if and only if there is a smooth coordinate chart $( V , \varphi )$ for S such that $X = \iota \circ \varphi ^ { - 1 }$ Therefore, every point of S is in the image of some local pa submersion, and the preceding corollary shows that $\phi ^ { - 1 } ( c )$ is an embedded submanifold of U .

Example 5.25

FC08-C05-U038 · Ch. 5, § Immersed Submanifolds; source L3053 · after FC08-C01-U006, FC08-C01-U008 · not formalized

(Graph Parametrizations). Suppose $U \subseteq \mathbb{R}^{n}$ is open and $f \colon U \to \mathbb{R}^{k}$ is smooth. The map $\gamma_{f} \colon U \to \mathbb{R}^{n} \times \mathbb{R}^{k}$ given by $\gamma_{f}(u) = (u, f(u))$ is a smooth global parametrization of $\Gamma(f)$, called a graph parametrization; its inverse is the graph coordinate map of Example 1.3. For instance $F \colon \mathbb{B}^{2} \to \mathbb{R}^{3}$, $F(u,v) = \left(u, v, \sqrt{1-u^{2}-v^{2}}\right)$, is a smooth local parametrization of $\mathbb{S}^{2}$ whose image is the open upper hemisphere.

Example 5.26

FC08-C05-U039 · Ch. 5, § Immersed Submanifolds; source L3061 · after FC08-C05-U033, FC08-C04-U019 · not formalized

Example 5.26 (Parametrization of the Figure-Eight Curve). Let $S \subseteq \mathbb { R } ^ { 2 }$ be the figure-eight curve of Example 5.19, considered as an immersed submanifold of $\mathbb { R } ^ { 2 }$ . The map $\beta \colon ( - \pi , \pi ) \to { \mathbb { R } } ^ { 2 }$ of Example 4.19 is a smooth global parametrization is at least locally of this form.

Theorem 5.27

FC08-C05-U040 · Ch. 5, § Restricting Maps to Submanifolds; source L3073 · not formalized

Theorem 5.27 (Restricting the Domain of a Smooth Map). If M and N are smooth manifolds with or without boundary, $F \colon M \to N$ is a smooth map, and $S \subseteq M$ is an immersed or embedded submanifold (Fig. 5.9), then $F | _ { S } \colon S \to N$

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib proves restriction/composition results for open subtypes and generic smooth maps, but has no arbitrary embedded/immersed-submanifold codomain/domain object and no weakly-embedded predicate. Consequently it cannot state the source restriction or uniqueness theorem at this level of generality; open-subtype lemmas are proper specializations. Strict bundle semantics reject a proper subset, isolated ingredient, unbridged equivalent notion, stronger-hypothesis specialization, or reconstruction of the substantive source theorem.

Example 5.28

FC08-C05-U041 · Ch. 5, § Restricting Maps to Submanifolds; source L3079 · after FC08-C04-U019 · not formalized

Let $S \subseteq \mathbb{R}^{2}$ be the figure-eight submanifold, with the topology and smooth structure induced by the immersion $\beta$ of Example 4.19, and define $G \colon \mathbb{R} \to \mathbb{R}^{2}$ by $G(t) = (\sin 2t,\ \sin t)$ — the formula defining $\beta$, extended to the whole real line. The image of $G$ lies in $S$, but as a map from $\mathbb{R}$ to $S$ it is not even continuous, because $\beta^{-1} \circ G$ is not continuous at $t = \pi$.

Theorem 5.29

FC08-C05-U042 · Ch. 5, § Restricting Maps to Submanifolds; source L3089 · not formalized

(Restricting the Codomain of a Smooth Map). Suppose $M$ is a smooth manifold without boundary, $S \subseteq M$ is an immersed submanifold, and $F \colon N \to M$ is a smooth map whose image is contained in $S$. If $F$ is continuous as a map from $N$ to $S$, then $F \colon N \to S$ is smooth.

Corollary 5.30

FC08-C05-U043 · Ch. 5, § Restricting Maps to Submanifolds; source L3108 · not formalized

Corollary 5.30 (Embedded Case). Let M be a smooth manifold and M$ be an embedded submanifold. Then every smooth map $F \colon N \to M$ whose image is contained in S is also smooth as a map from N to $

Definition/convention — initial submanifolds by some authors

FC08-C05-U044 · Ch. 5, § Restricting Maps to Submanifolds; source L3112 · after FC08-C05-U041, FC08-C05-U043 · not formalized

Although the conclusion of the preceding corollary fails for some immersed submanifolds such as the figure-eight curve (see Example 5.28), it turns out that there are certain immersed but nonembedded submanifolds for which it holds. To distinguish them, we introduce the following definition. If M is a smooth manifold and $S \subseteq M$ is an immersed submanifold, then S is said to be weakly embedded in M if every smooth map F N M whose image lies in S is smooth as a map from N to S. (Weakly embedded submanifolds are called initial submanifolds by some authors.) Corollary 5.30 shows that every embedded submanifold is weakly embedded. It follows from Example 5.28 that the figure-eight curve is not weakly embedded. However, the dense curve on the torus is weakly embedded; see Problem 5-13. In Chapter 19, we will encounter some classes of submanifolds that are automatically weakly embedded (see Theorems 19.17 and 19.25). ##

Theorem 5.31

FC08-C05-U045 · Ch. 5, § Uniqueness of Smooth Structures on Submanifolds; source L3120 · after FC08-C05-U014 · not formalized

Theorem 5.31. Suppose M is a smooth manifold and $S \subseteq M$ is an embedded submanifold. The subspace topology on S and the smooth structure described in Theorem 5.8 are the only topology and smooth structure with respect to which S is an embedded or immersed submanifold.

Theorem 5.32

FC08-C05-U046 · Ch. 5, § Uniqueness of Smooth Structures on Submanifolds; source L3134 · not formalized

Theorem 5.32. Suppose M is a smooth manifold and $S \subseteq M$ is an immersed submanifold. For the given topology on S, there is only one smooth structure making S into an immersed submanifold.

Theorem 5.33

FC08-C05-U047 · Ch. 5, § Uniqueness of Smooth Structures on Submanifolds; source L3140 · not formalized

Theorem 5.33. If M is a smooth manifold and $S \subseteq M$ is a weakly embedded submanifold, then S has only one topology and smooth structure with respect to which it is an immersed submanifold.

Convention/notation — source terminology/construction

FC08-C05-U048 · Ch. 5, § Extending Functions from Submanifolds; source L3146 · not formalized

Complementary to the restriction problem is the problem of extending smooth functions from a submanifold to the ambient manifold. Let M be a smooth manifold with or without boundary, and let $S \subseteq M$ be a smooth submanifold. If $f \colon S \to \mathbb { R }$ is a function, there are two ways we might interpret the statement “f is smooth”: it might mean that f is smooth as a function on the smooth manifold S (i.e., each coordinate representation is smooth), or it might mean that it is smooth as a function on the subset $S \subseteq M$ (i.e., it admits a smooth extension to a neighborhood of each point). We adopt the convention that the notation $f \in C ^ { \infty } ( S )$ always means that f is smooth in the former sense (as a function on the mani 4.19 and the dense curve of Example 4.20 are images of injective smooth immersions, they are immersed submanifolds when given appropriate topologies and smooth structures.

Not formalized. none; no complete checked declaration under strict bundle semantics — Smooth-function restriction, partitions of unity, TangentSpace, and mfderiv exist, but the missing submanifold object prevents the required extension theorem and tangent-space identification/annihilator/kernel characterizations. No checked declaration bridges the tangent space of an arbitrary embedded/immersed subset to the ambient tangent space. Strict bundle semantics reject a proper subset, isolated ingredient, unbridged equivalent notion, stronger-hypothesis specialization, or reconstruction of the substantive source theorem.

Lemma 5.34

FC08-C05-U049 · Ch. 5, § Extending Functions from Submanifolds; source L3148 · not formalized

Lemma 5.34 (Extension Lemma for Functions on Submanifolds). Suppose M is a smooth manifold, $S \subseteq M$ is a smooth submanifold, } ( S )$ (a) If S is embedded, then there exist a neighborhood U of S in M and a smooth function ${ such that $\widetilde f | _ { S } = f$ (b) If S is properly embedded, then the neighborhood U in part (a) can be taken s and smooth structures (see Problems 5-4 and 5-5).

Definition/convention — source terminology/construction

FC08-C05-U050 · Ch. 5, § The Tangent Space to a Submanifold; source L3165 · not formalized

Let M be a smooth manifold with or without boundary, and let $S \subseteq M$ be an immersed or embedded submanifold. Since the inclusion map $\iota \colon S \hookrightarrow M$ is a smooth immersion, at each point $p \in S$ we have an injective linear map $d \iota _ { p } \colon T _ { p } S \to T _ { p } M$ In terms of derivations, this injection works in the following way: for any vector $v \in T _ { p } S$ , the image vector $\boldsymbol { \widetilde { v } } = d \iota _ { p } ( \boldsymbol { v } ) \in T _ { p } \boldsymbol { M }$ acts on smooth functions on M by \[ \widetilde {v} f = d \iota_ {p} (v) f = v (f \circ \iota) = v (f | _ {S}). \]

Proposition 5.35

FC08-C05-U051 · Ch. 5, § The Tangent Space to a Submanifold; source L3175 · not formalized

Proposition 5.35. Suppose M is a smooth manifold with or without boundary, $S \subseteq M$ is an immersed or embedded submanifold, and $p \in S$ . A vector $v \in T _ { p } M$ is in $T _ { p } S$ if and only if there is a smooth curve J M whose image is contained in S, and which is also smooth as a map into S, such that $0 \in J , \gamma ( 0 ) = p .$ , and $\gamma ^ { \prime } ( 0 ) = v$

Proposition 5.37

FC08-C05-U052 · Ch. 5, § The Tangent Space to a Submanifold; source L3181 · not formalized

Suppose $M$ is a smooth manifold, $S \subseteq M$ is an embedded submanifold and $p \in S$. As a subspace of $T_{p}M$, the tangent space is characterized by \[ T_{p}S = \{v \in T_{p}M : vf = 0 \text{ whenever } f \in C^{\infty}(M) \text{ and } f|_{S} = 0\}. \]

Proposition 5.38

FC08-C05-U053 · Ch. 5, § The Tangent Space to a Submanifold; source L3217 · not formalized

Suppose $M$ is a smooth manifold and $S \subseteq M$ is an embedded submanifold. If $\Phi \colon U \to N$ is any local defining map for $S$, then $T_{p}S = \operatorname{Ker}\left(d\Phi_{p} \colon T_{p}M \to T_{\Phi(p)}N\right)$ for each $p \in S \cap U$.

Corollary 5.39

FC08-C05-U054 · Ch. 5, § The Tangent Space to a Submanifold; source L3229 · not formalized

Suppose $S \subseteq M$ is a level set of a smooth submersion $\Phi = (\Phi^{1},\dots,\Phi^{k}) \colon M \to \mathbb{R}^{k}$. A vector $v \in T_{p}M$ is tangent to $S$ if and only if $v\Phi^{1} = \cdots = v\Phi^{k} = 0$.

Definition/convention — inwardpointing

FC08-C05-U055 · Ch. 5, § The Tangent Space to a Submanifold; source L3234 · not formalized

If M is a smooth manifold with boundary and $p \in \partial M$ ; it is intuitively evident that the vectors in $T _ { p } M$ can be separated into three classes: those tangent to the boundary, those pointing inward, and those pointing outward. Formally, we make the following definition. If $p \in \partial M ,$ a vector $v \in T _ { p } M \setminus T _ { p } \partial M$ is said to be inwardpointing if for some $\varepsilon > 0$ there exists a smooth curve $\gamma \colon [ 0 , \varepsilon ) \to M$ such that $\gamma ( 0 ) = p$ and $\gamma ^ { \prime } ( 0 ) = v$ , and it is outward-pointing if there exists such a curve whose domain is $( - \varepsilon , 0 ] .$ The following proposition gives another characterization of inward-pointing and outward-pointing vectors, which is usually much easier to check. (See Fig.

Not formalized. none; no complete checked declaration under strict bundle semantics — InteriorBoundary.lean formalizes interior/boundary points as sets but has no inward/outward tangent-vector API, boundary defining functions, or theorem producing one. Its TODO explicitly records the missing boundary-as-submanifold layer, so the source row cannot be expressed completely in the checked manifold interface. Strict bundle semantics reject a proper subset, isolated ingredient, unbridged equivalent notion, stronger-hypothesis specialization, or reconstruction of the substantive source theorem.

Proposition 5.41

FC08-C05-U056 · Ch. 5, § The Tangent Space to a Submanifold; source L3236 · not formalized

Proposition 5.41. Suppose M is a smooth n-dimensional manifold with boundary, $p \in \partial M .$ ; and $\left( x ^ { i } \right)$ are any smooth boundary coordinates defined on a neighborhood of p. The inward-pointing vectors in $T _ { p } M$ are precisely those with positive $x ^ { n }$ -component, the outward-pointing ones are those with negative $x ^ { n }$ -component, and the ones tangent to @M are those with zero $x ^ { n }$ -component. Thus, $T _ { p }$ M is the disjoint union of $T _ { p } \partial M ,$ ; the set of inward-pointing vectors, and the set of outwardpointing vectors, and $v \in T _ { p } M$ is inward-pointing if and only $i f - v$ is outwardpointing.

Definition/convention — boundary defining function for M

FC08-C05-U057 · Ch. 5, § The Tangent Space to a Submanifold; source L3240 · not formalized

Proposition 5.41. If M is a smooth manifold with boundary, a boundary defining function for M is a smooth function $f \colon M \to [ 0 , \infty )$ such that $f ^ { - 1 } ( 0 ) = \partial M$ and $d f _ { p } \neq 0$ for all $p \in \partial M$ . For example, $f ( x ) = 1 - | x | ^ { 2 }$ is a boundary defining function for the closed unit ball $\mathbf { \overline { { B } } } ^ { n } \mathbf { . }$

Proposition 5.43

FC08-C05-U058 · Ch. 5, § The Tangent Space to a Submanifold; source L3242 · not formalized

Every smooth manifold with boundary admits a boundary defining function.

Example 5.45

FC08-C05-U059 · Ch. 5, § The Tangent Space to a Submanifold; source L3268 · after FC08-C05-U051 · not formalized

Consider $S = \{(x,y) : y = |x|\} \subseteq \mathbb{R}^{2}$. Since $S \setminus \{(0,0)\}$ is an embedded 1-dimensional submanifold of $\mathbb{R}^{2}$, if $S$ itself were a smooth submanifold it would be 1-dimensional. Differentiating twice and setting $t = 0$ gives $2x'(0)^{2} = 2y'(0)^{2} = 0$, a contradiction; so no such smooth manifold structure exists.

Definition/convention — embedded submanifold

FC08-C05-U060 · Ch. 5, § Submanifolds with Boundary; source L3275 · not formalized

So far in this chapter, all of our submanifolds have been manifolds without boundary. For some purposes (notably in the theory of integration), it is important also to consider submanifolds that have boundaries. The definitions are straightforward generalizations of the ones for ordinary submanifolds. If M is a smooth manifold with or without boundary, a smooth submanifold with boundary in M is a subset $S \subseteq M$ endowed with a topology and smooth structure making it into a smooth manifold with boundary such that the inclusion map is a smooth immersion. If the inclusion map is an embedding, then it is called an embedded submanifold with boundary; in the general case, it is an immersed submanifold with boundary. The terms codimension and properly embedded are defined just as in the submanifold case.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has models with corners, interval/half-space examples, smooth embeddings, and interior/boundary sets, but no general submanifold-with-boundary, regular-domain, half-slice, regular-sublevel, or restricting-maps-to-submanifolds package. The checked current upstream also has no such file/interface, so the complete source row remains unmatched. Strict bundle semantics reject a proper subset, isolated ingredient, unbridged equivalent notion, stronger-hypothesis specialization, or reconstruction of the substantive source theorem.

Definition/convention — regular domain in M

FC08-C05-U061 · Ch. 5, § Submanifolds with Boundary; source L3279 · not formalized

5.14). One particular type of submanifold with boundary is especially important. If M is a smooth manifold with or without boundary, a regular domain in M is a properly embedded codimension-0 submanifold with boundary. Familiar examples are the closed upper half space $\mathbb { H } ^ { n } \subseteq \mathbb { R } ^ { n }$ , the closed unit ball ${ \overline { { \mathbb { B } } } } ^ { n } \subseteq \mathbb { R } ^ { n }$ , and the closed up 10d8a9db26a26a3852647dacde61254.jpg) Fig.

Proposition 5.46

FC08-C05-U062 · Ch. 5, § Submanifolds with Boundary; source L3281 · not formalized

closed upper hemisphere in ${ \overline { { \mathbb { S } ^ { n } } } } .$ Proposition 5.46. Suppose M is a smooth manifold without boundary and $D \subseteq M$ is a regular domain. The topological interior and boundary of D are equal to its manifold interior and boundary, r

Proposition 5.47

FC08-C05-U063 · Ch. 5, § Submanifolds with Boundary; source L3297 · not formalized

Suppose $M$ is a smooth manifold and $f \in C^{\infty}(M)$.

Not formalized. none; no complete checked declaration under strict bundle semantics — The canonical Sweep-I row is itself incomplete: its statement ends after Suppose M is a smooth manifold and f ∈ C^∞(M). No theorem conclusion is present to route. Sweep II does not reconstruct or silently repair canonical source units from an external copy of the book. Strict bundle semantics reject a proper subset, isolated ingredient, unbridged equivalent notion, stronger-hypothesis specialization, or reconstruction of the substantive source theorem.

Definition/convention — regular sublevel set of f

FC08-C05-U064 · Ch. 5, § Submanifolds with Boundary; source L3299 · not formalized

of the form $f ^ { - 1 } \bigl ( ( - \infty , b ] \bigr )$ for b a regular value of f is called a regular sublevel set of f . Part (a) of the preceding theorem shows that every regular sublevel set of a smooth real-valued function is a regular domain. If $D \subseteq M$ is a regular domain and $f \in C ^ { \infty } ( M )$ is a smooth function such that D is a regular sublevel set of f , then f is called a defining function for $D$.

Theorem 5.48

FC08-C05-U065 · Ch. 5, § Submanifolds with Boundary; source L3301 · not formalized

Theorem 5.48. If M is a smooth manifold and $D \subseteq M$ is a regular domain, then there exists a defining function for D. If D is compact, then f can be taken to be a smooth exhaustion function for M .

Proposition 5.49

FC08-C05-U066 · Ch. 5, § Submanifolds with Boundary; source L3307 · not formalized

Proposition 5.49 (Properties of Submanifolds with Boundary). Suppose M is a smooth manifold with or without boundary. (a) Every open subset of M is an embedded codimension-0 submanifold with (possibly empty) boundary. (b) If N is a smooth manifold with boundary and $F \colon N \to M$ is a smooth embedding, then with the subspace topology F .N / is a topological manifold with boundary, and it has a smooth structure making it into an embedded submanifold with boundary in M . (c) An embedded submanifold with boundary in M is properly embedded if and only if it is closed. (d) If $S \subseteq M$ is an immersed submanifold with boundary, then for each $p \in S$ there exists a neighborhood U of p in S that is embedded , and consider the function $f ( x ) = \varphi ( x ) x ^ { j }$ extended to be zero on $M \setminus \operatorname { s u p p } \varphi$ .

Definition/convention — k-dimensional halfslice of U

FC08-C05-U067 · Ch. 5, § Submanifolds with Boundary; source L3319 · not formalized

In order to adapt the results that depended on the existence of local slice charts, we have to generalize the local k-slice condition as follows. Suppose M is a smooth manifold (without boundary). If $\left( U , \left( x ^ { i } \right) \right)$ is a chart for M; a k-dimensional halfslice of U is a subset of the following form for some constants defining map gives a concise characterization of its tangent space at each point, as the next proposition shows.

Definition/convention — interior slice chart for S in M

FC08-C05-U068 · Ch. 5, § Submanifolds with Boundary; source L3325 · not formalized

We say that a subset $S \subseteq M$ satisfies the local $\scriptstyle { k - s l i c e }$ condition for submanifolds with boundary if each point of S is contained in the domain of a smooth chart $\left( U , \left( x ^ { i } \right) \right)$ such that $S \cap U$ is either an ordinary k-dimensional slice or a k-dimensional half-slice. In the former case, the chart is called an interior slice chart for S in M , and in the latter, it is a boundary slice chart.

Theorem 5.51

FC08-C05-U069 · Ch. 5, § Submanifolds with Boundary; source L3327 · not formalized

Theorem 5.51. Let M be a smooth n-manifold without boundary. If $S \subseteq M$ is an embedded k-dimensional submanifold with boundary, then S satisfies the local k-slice condition for submanifolds with boundary. Conversely, if $S \subseteq M$ is a subset that satisfies the local k-slice condition for submanifolds with boundary, then with the subspace topology, S is a topological k-manifold with boundary, and it has a smooth structure making it into an embedded submanifold with boundary in M .

Theorem 5.53

FC08-C05-U070 · Ch. 5, § Submanifolds with Boundary; source L3333 · not formalized

(Restricting Maps to Submanifolds with Boundary). Suppose $M$ and $N$ are smooth manifolds with boundary and $S \subseteq M$ is an embedded submanifold with boundary. (a) Restricting the domain: if $F \colon M \to N$ is smooth, then $F|_{S} \colon S \to N$ is smooth. (b) Restricting the codomain: if $\partial M = \emptyset$ and $F \colon N \to M$ is a smooth map whose image is contained in $S$, then $F$ is smooth as a map from $N$ to $S$.