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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 8 definitions, 15 theorems, 5 propositions, 5 lemmas, 9 corollaries, 1 construction and 1 convention.

Of the 44 statements checked against Lean, 3 are formalized somewhere and 41 are not.

Status	Statements	Share	What it means
not formalized	41	93%	A documented search found no Lean statement of it anywhere.
in Mathlib	3	7%	Mathlib states and proves it.
checked in total	44

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 6, FC08-C06-U001–FC08-C06-U044, exactly 44 unique contiguous rows retrieved from FC08 — John M. Lee, Introduction to Smooth Manifolds through agent-memory.
Chapter title: Sard’s Theorem. 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 current/indexed/external Lean searches and local reference probes. No project-existing, package-import, or completed reference-port C06 owner survived strict checking.
C06 has 3 pinned mathlib rows and 41 dated unmatched rows. Positive rows are U003, U023, U024. Every cited positive file exists at exact P. /tmp/fc08-c06-witness.lean compiles U003’s Euclidean specialization of addHaar_affineSubspace and derives U024 exactly from Continuous.exists_contMDiff_approx; it also confirms the relevant smooth-approximation interface at the project pin. The witness is audit evidence only, not project source.
U003 is direct measure theory: addHaar_affineSubspace proves every proper affine subspace of a finite-dimensional real normed space is null for any additive Haar measure, hence for Euclidean volume. U023 is the pinned SmoothApprox theorem: variable positive continuous error, smooth approximation of a continuous vector-valued function on a real finite-dimensional manifold, with equality on a closed set where the original map is already smooth on a neighborhood. U024 is the immediate positive smooth minorant corollary, compiled from U023.
P/H do not have Lee’s manifold measure-zero abstraction. An external indexed search found fpvandoorn/sard, inspected at R=77da83ff581fc9bf8af67e18ba8949cf555cc41c (Lean 4.12.0). Its completed Sard/MeasureZero.lean defines a preferred-chart MeasureZero, but the file explicitly notes that equivalence with all charts is still missing; measure_zero_image_iff_chart_domains itself contains sorry. Therefore U005–U008 are not promoted from that repository.
The same external repository is not used as a Sard reference-port: its README states the hard Morse–Sard case remains open, and the exact checkout contains 41 sorry/admit occurrences. Sard/MainTheorem.lean states manifold Sard results but their proofs depend on those unfinished obligations. P/H only provide partial Euclidean/Hausdorff-dimension Sard consequences, so U009–U010 remain unmatched.
Mathlib/Geometry/Manifold/WhitneyEmbedding.lean is deliberately not over-credited. At P and H it proves a compact-manifold embedding into some finite-dimensional Euclidean space and explicitly lists the general weak ℝ^(2m+1) theorem as TODO pending stronger Sard machinery. Thus none of U013–U021 has the dimension-sharp/general owner demanded by Lee’s rows.
Mathlib/Geometry/Manifold/SmoothApprox.lean is a direct owner only for U023 and the compiled U024 corollary. It does not approximate maps into arbitrary manifold codomains and does not produce homotopies, so U030–U034 remain unmatched. U022 is only terminology: Mathlib uses the same pointwise distance formula but exposes no named ε-close predicate.
Targeted P/H searches found no tubular-neighborhood implementation, no normal-bundle construction for arbitrary embedded submanifolds, and no smooth transversality API. The latter appears only in comments in Bordism.lean; there is no checked Transverse predicate or parametric/transversality-homotopy theorem. Consequently U025–U029 and U035–U044 remain unmatched. These blocks also depend on the general submanifold abstraction already established missing in C05.
Current upstream H was inspected by git object without changing the pinned worktree. H still contains only SmoothApprox.lean and WhitneyEmbedding.lean among the relevant manifold files, and targeted searches found no Sard-manifold, tubular, transversality, or smooth-homotopy implementation.
N=2026-09-07 marks dated unmatched decisions after the prescribed search layers. Strict whole-row semantics apply uniformly.

Lemma 6.2

FC08-C06-U001 · Ch. 6, § Sets of Measure Zero; source L3446 · not formalized

Suppose $A \subseteq \mathbb{R}^{n}$ is a compact subset whose intersection with $\{c\} \times \mathbb{R}^{n-1}$ has $(n-1)$-dimensional measure zero for every $c \in \mathbb{R}$. Then $A$ has $n$-dimensional measure zero.

Not formalized. none; no complete checked declaration under strict bundle semantics — Product-measure/Fubini and measurable-set primitives are present, but no checked declaration owns Lee’s exact Euclidean slice/continuous-graph nullity statement as a whole. Reconstructing the coordinate/product identification and measurability argument would be new proof work rather than locating an existing interface. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unfinished/sorry-dependent sources, isolated ingredients, and reconstruction of the substantive source theorem.

Proposition 6.3

FC08-C06-U002 · Ch. 6, § Sets of Measure Zero; source L3457 · not formalized

Proposition 6.3. Suppose A is an open or closed subset of $\mathbb { R } ^ { n - 1 } ~ o r ~ \mathbb { H } ^ { n - 1 }$ , and $f \colon A \to \mathbb { R }$ is a continuous function. Then the graph of f has measure zero in $\mathbb{R}^{n}$.

Corollary 6.4

FC08-C06-U003 · Ch. 6, § Sets of Measure Zero; source L3463 · in Mathlib

Every proper affine subspace of $\mathbb{R}^{n}$ has measure zero in $\mathbb{R}^{n}$.

Formalized. Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean::addHaar_affineSubspace — The pinned theorem is strictly more general: every proper affine subspace of any finite-dimensional real normed space has zero additive-Haar measure. Specializing to Euclidean space with volume gives Lee’s claim exactly; the specialization compiled in /tmp/fc08-c06-witness.lean.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Proposition 6.5

FC08-C06-U004 · Ch. 6, § Sets of Measure Zero; source L3469 · not formalized

Suppose $A \subseteq \mathbb{R}^{n}$ has measure zero and $F \colon A \to \mathbb{R}^{n}$ is a smooth map. Then $F(A)$ has measure zero.

Not formalized. none; no complete checked declaration under strict bundle semantics — addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero maps null subsets to null subsets for an ambient differentiable self-map, but Lee’s row is stated for a smooth map defined only on an arbitrary null subset. The checked library has no source predicate/bridge packaging Lee’s locally extendable smooth-on-a-subset notion, so the direct theorem is only a proper specialization. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unfinished/sorry-dependent sources, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — source terminology/construction

FC08-C06-U005 · Ch. 6, § Sets of Measure Zero; source L3486 · not formalized

If M is a smooth n-manifold with or without boundary, we say that a subset $A \subseteq M$ has measure zero in M if for every smooth chart $( U , \varphi )$ for M; the subset $\varphi ( A \cap U ) \subseteq \mathbb { R } ^ { n }$ has n-dimensional measure zero. The following lemma shows that we need only check this condition for a single collection of smooth charts whose domains cove frac {}{r} | _ {p} - | _ {p}.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has no manifold-level measure-zero predicate matching Lee’s all-charts definition. The external fpvandoorn/sard repository at R defines a preferred-chart MeasureZero, and its own source notes that equivalence with all charts is still missing; its later chart-cover theorem also contains sorry. Hence none of these manifold null-set rows has a completed exact owner. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unfinished/sorry-dependent sources, isolated ingredients, and reconstruction of the substantive source theorem.

Lemma 6.6

FC08-C06-U006 · Ch. 6, § Sets of Measure Zero; source L3488 · not formalized

Lemma 6.6. Let M be a smooth n-manifold with or without boundary and $A \subseteq M$ Suppose that for some collection $\{ ( U _ { \alpha } , \varphi _ { \alpha } ) \}$ of smooth charts whose domains cover A, $\varphi _ { \alpha } ( A \cap U _ { \alpha } )$ has measure zero in $\mathbb { R } ^ { n }$ for each ˛. Then A has measure zero ded submanifold).

Proposition 6.8

FC08-C06-U007 · Ch. 6, § Sets of Measure Zero; source L3500 · not formalized

Proposition 6.8. Suppose M is a smooth manifold with or without boundary and $A \subseteq M$ has measure zero in M . Then M A is dense in M .

Theorem 6.9

FC08-C06-U008 · Ch. 6, § Sets of Measure Zero; source L3504 · not formalized

Theorem 6.9. Suppose M and N are smooth n-manifolds with or without boundary, $F \colon M \to N$ is a smooth map, and $A \subseteq M$ is a subset of measure zero. Then $F ( A )$ has measure zero in $N$.

Theorem 6.10

FC08-C06-U009 · Ch. 6, § Sard’s Theorem; source L3516 · not formalized

Theorem 6.10 (Sard’s Theorem). Suppose M and N are smooth manifolds with or without boundary and $F: M \to N$ is a smooth map. Then the set of critical values of F has measure zero in N.

Not formalized. none; no complete checked declaration under strict bundle semantics — Full Morse–Sard for manifolds is not in P or H. Mathlib has only fixed-dimensional/low-dimensional Hausdorff-dimension consequences. The external fpvandoorn/sard project states the manifold theorem but its hard case remains unfinished and the relevant files contain sorry, so it is not a valid reference-port formalization. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unfinished/sorry-dependent sources, isolated ingredients, and reconstruction of the substantive source theorem.

Corollary 6.11

FC08-C06-U010 · Ch. 6, § Sard’s Theorem; source L3583 · not formalized

Corollary 6.11. Suppose M and N are smooth manifolds with or without boundary, and $F \colon M \to N$ is a smooth map. If dim M < dim N , then F .M / has measure zero that $A_c \subseteq U_c$.

Definition/convention — space-filling curve

FC08-C06-U011 · Ch. 6, § Sard’s Theorem; source L3589 · after FC08-C06-U010 · not formalized

It is important to be aware that Corollary 6.11 is false if F is merely assumed to be continuous. For example, there is a continuous map $F \colon [ 0 , 1 ] \to \mathbb { R } ^ { 2 }$ ] $ . (Such a map is called a space-filling curve. See [Rud76, p. 168] for an example.) Corollary 6.12. Suppose M is a smooth manifold with or without boundary, and $

Not formalized. none; no complete checked declaration under strict bundle semantics — The checked sources have continuous surjections and Peano/space-filling-adjacent topology ingredients, but no named space-filling curve construction/interface realizing the unit-square example in this row. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unfinished/sorry-dependent sources, isolated ingredients, and reconstruction of the substantive source theorem.

Corollary 6.12

FC08-C06-U012 · Ch. 6, § Sard’s Theorem; source L3591 · not formalized

Corollary 6.12. Suppose M is a smooth manifold with or without boundary, and $S \subseteq M$ is an immersed submanifold with or without boundary. If dim S < dim M; then S has measure zero in M .

Not formalized. none; no complete checked declaration under strict bundle semantics — This conclusion needs both Lee’s manifold measure-zero predicate and a general immersed-submanifold package. C05 established that the checked P/H interface has neither exact abstraction, so the lower-dimensional immersed-submanifold nullity statement cannot be expressed as a complete existing theorem. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unfinished/sorry-dependent sources, isolated ingredients, and reconstruction of the substantive source theorem.

Lemma 6.13

FC08-C06-U013 · Ch. 6, § The Whitney Embedding Theorem; source L3601 · not formalized

Suppose $M \subseteq \mathbb{R}^{N}$ is a smooth $n$-dimensional submanifold with or without boundary. For $v \in \mathbb{R}^{N} \setminus \mathbb{R}^{N-1}$, let $\pi_{v} \colon \mathbb{R}^{N} \to \mathbb{R}^{N-1}$ be the projection with kernel $\mathbb{R}v$, identifying $\mathbb{R}^{N-1}$ with the points of $\mathbb{R}^{N}$ whose last coordinate is zero. If $N > 2n+1$, there is a dense set of vectors $v \in \mathbb{R}^{N} \setminus \mathbb{R}^{N-1}$ for which $\pi_{v}|_{M}$ is an injective immersion of $M$ into $\mathbb{R}^{N-1}$.

Not formalized. none; no complete checked declaration under strict bundle semantics — WhitneyEmbedding.lean proves only a baby/compact Whitney result: a compact real manifold embeds in some finite-dimensional Euclidean space. Its TODO explicitly says the general weak 2m+1 theorem still requires missing Sard machinery. It therefore does not own Lee’s dimension-sharp projection, proper embedding, immersion, strong Whitney, approximation-by-embeddings, or nomenclature row. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unfinished/sorry-dependent sources, isolated ingredients, and reconstruction of the substantive source theorem.

Lemma 6.14

FC08-C06-U014 · Ch. 6, § The Whitney Embedding Theorem; source L3615 · not formalized

Let $M$ be a smooth $n$-manifold with or without boundary. If $M$ admits a smooth embedding into $\mathbb{R}^{N}$ for some $N$, then it admits a proper smooth embedding into $\mathbb{R}^{2n+1}$.

Theorem 6.15

FC08-C06-U015 · Ch. 6, § The Whitney Embedding Theorem; source L3634 · not formalized

(Whitney Embedding Theorem). Every smooth $n$-manifold with or without boundary admits a proper smooth embedding into $\mathbb{R}^{2n+1}$.

Corollary 6.16

FC08-C06-U016 · Ch. 6, § The Whitney Embedding Theorem; source L3678 · not formalized

Corollary 6.16. Every smooth n-dimensional manifold with or without boundary is diffeomorphic to a properly embedded submanifold (with or without boundary)

Corollary 6.17

FC08-C06-U017 · Ch. 6, § The Whitney Embedding Theorem; source L3680 · not formalized

Corollary 6.17. Suppose M is a compact smooth n-manifold with or withou boundary. If $N \geq 2 n + 1$ , then every smooth map from M to $\mathbb { R } ^ { N }$ can be uniformly approximated by embeddi kth partial derivative of F that has at least one nonvanishing first partial derivative at a.

Theorem 6.18

FC08-C06-U018 · Ch. 6, § The Whitney Embedding Theorem; source L3686 · not formalized

(Whitney Immersion Theorem). Every smooth $n$-manifold with or without boundary admits a smooth immersion into $\mathbb{R}^{2n}$.

Theorem 6.19

FC08-C06-U019 · Ch. 6, § The Whitney Embedding Theorem; source L3694 · not formalized

Theorem 6.19 (Strong Whitney Embedding Theorem). If $n > 0$ , every smooth n-manifold admits a smooth embedding into $\mathbb { R } ^ { 2 n }$

Theorem 6.20

FC08-C06-U020 · Ch. 6, § The Whitney Embedding Theorem; source L3696 · not formalized

Theorem 6.20 (Strong Whitney Immersion Theorem). If $n > 1$ , every smooth n-manifold admits a smooth immersion into $\mathbb { R } ^ { 2 n - 1 }$

Convention/notation — weak/easy Whitney theorems

FC08-C06-U021 · Ch. 6, § The Whitney Embedding Theorem; source L3698 · not formalized

Because of these results, Theorems 6.15 and 6.18 are sometimes called the easy or weak Whitney embedding and immersion theorems. I

Definition/convention — source terminology/construction

FC08-C06-U022 · Ch. 6, § The Whitney Approximation Theorems; source L3706 · not formalized

We begin with a theorem about smoothly approximating functions into Euclidean spaces. Our first theorem shows, in particular, that any continuous function from a smooth manifold M into $\mathbb { R } ^ { k }$ can be uniformly approximated by a smooth function. In fact, we will prove something stronger. $\mathrm { I f ~ } \delta \colon M \mathbb { R }$ is a positive continuous function, we say { F } ^ { k }$ are ı-close if $|

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib uses the pointwise inequality dist (g x) (f x) < ε x throughout SmoothApprox.lean, but does not package Lee’s “ε-close” terminology as a named definition/interface. The raw formula is an ingredient rather than an owner of this terminology row. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unfinished/sorry-dependent sources, isolated ingredients, and reconstruction of the substantive source theorem.

Theorem 6.21

FC08-C06-U023 · Ch. 6, § The Whitney Approximation Theorems; source L3708 · in Mathlib

if $\left| F ( x ) - { \widetilde F } ( x ) \right| <$ ı.x/ for all $x \in M .$ Theorem 6.21 (Whitney Approximation Theorem for Functions). Suppose M is a smooth manifold with or without boundary, and $F \colon M \to \mathbb { R } ^ { k }$ is a continuous function. Given any positive continuous function ı M R, there exists a smooth function $\widetilde { F } \colon M \to \overline { { \mathbb { R } } } ^ { k }$ that is ı-close to F . If F is smooth on a closed subset $A \subseteq M .$ then $\widetilde { F }$ can be chosen to be equal to F on A. Proof. If F is smooth on the closed subset A, then by the extension lemma for smooth functions (Lemma 2.26), there is a smooth function $F _ { 0 } \colon M \to \mathbb { R } ^ { k }$

Formalized. Mathlib/Geometry/Manifold/SmoothApprox.lean::Continuous.exists_contMDiff_approx_and_eqOn — This is Lee’s Whitney approximation theorem for real-valued/vector-valued functions in the same variable-precision form: a continuous map from a finite-dimensional real manifold to a normed space is approximated by a C^n map within a prescribed positive continuous ε, with equality on a closed set where the original map is already smooth on a neighborhood. Lee’s manifold conventions supply the Hausdorff/σ-compact hypotheses used explicitly by Mathlib.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Corollary 6.22

FC08-C06-U024 · Ch. 6, § The Whitney Approximation Theorems; source L3750 · in Mathlib

If $M$ is a smooth manifold with or without boundary and $\delta \colon M \to \mathbb{R}$ is a positive continuous function, there is a smooth function $\varepsilon \colon M \to \mathbb{R}$ with $0 < \varepsilon(x) < \delta(x)$ for all $x \in M$.

Formalized. Mathlib/Geometry/Manifold/SmoothApprox.lean::Continuous.exists_contMDiff_approx — Applying the pinned approximation theorem to δ/2 with error δ/2 gives a smooth real function e satisfying 0 < e < δ pointwise. This exact corollary was compiled in /tmp/fc08-c06-witness.lean.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Construction/definition — normal space to M at x to be the ( n - m ) -dimensional subsp

FC08-C06-U025 · Ch. 6, § Tubular Neighborhoods; source L3758 · not formalized

For each $x \in \mathbb { R } ^ { n }$ , the tangent space $T _ { x } \mathbb { R } ^ { n }$ is canonically identified with $\mathbb { R } ^ { n }$ itself, and the tangent bundle $T \mathbb { R } ^ { n }$ is canonically diffeomorphic to $\mathbb { R } ^ { n } \times \mathbb { R } ^ { n }$ . By virtue of this identification, each tangent space $T _ { x } \mathbb { R } ^ { n }$ inherits a Euclidean dot product. Suppose $M \subseteq \mathbb { R } ^ { n }$ is an embedded m-dimensional submanifold. For each $x \in M ,$ we define the normal space to M at x to be the $( n - m )$ -dimensional subspace $N _ { x } M \subseteq T _ { x } \mathbb { R } ^ { n }$ consisting of all vectors that are orthogonal to $T _ { x } M$ with respect to the Euclidean dot product. The normal bundle of M , denoted by NM; is the subset of $T \mathbb { R } ^ { n } \approx \mathbb { R } ^ { n } \times \mathbb { R } ^ { n }$ consisting of vectors that are normal to $M \colon$ \[ N M = \left\{(x, v) \in \mathbb {R} ^ {n} \times \mathbb {R} ^ {n}: x \in M, v \in N _ {x} M \right\}. \] There is a natural projection $\pi \colon NM \to M$ sending $(x,v)$ to $x$.

Not formalized. none; no complete checked declaration under strict bundle semantics — The checked manifold library has tangent-space and inner-product primitives but no general embedded-submanifold normal bundle or tubular-neighborhood construction. Targeted P/H searches find no tubular-neighborhood file/interface, and the external indexed result was a roadmap/reference note rather than Lean formalization. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unfinished/sorry-dependent sources, isolated ingredients, and reconstruction of the substantive source theorem.

Theorem 6.23

FC08-C06-U026 · Ch. 6, § Tubular Neighborhoods; source L3766 · not formalized

Theorem 6.23. If $M \subseteq \mathbb { R } ^ { n }$ is an embedded m-dimensional submanifold, then NM is an embedded n-dimensional submanifold of $T \mathbb { R } ^ { n } \approx \mathbb { R } ^ { n } \times \mathbb { R } ^ { n }$

Theorem 6.24

FC08-C06-U027 · Ch. 6, § Tubular Neighborhoods; source L3815 · not formalized

Theorem 6.24 (Tubular Neighborhood Theorem). Every embedded submanifold $o f \mathbb { R } ^ { n }$ has a tubular neighborh s that F is a smooth embedding.

Definition/convention — source terminology/construction

FC08-C06-U028 · Ch. 6, § Tubular Neighborhoods; source L3843 · not formalized

Proposition 4.6. Therefore, $U$ is a tubular neighborhood of M . One of the most useful features of tubular neighborhoods is expressed in the next proposition. A retraction of a topological space X onto a subspace $M \subseteq X$ is a continuous map r X M such that $r | _ { M }$ is the identity map of M . ##

Proposition 6.25

FC08-C06-U029 · Ch. 6, § Tubular Neighborhoods; source L3845 · not formalized

Proposition 6.25. Let $M \subseteq \mathbb { R } ^ { n }$ be an embedded submanifold. If U is any tubular neighborhood of M; there exists a smooth map $r \colon U \to M$ that is both a retraction and a smooth su is an embedding.

Theorem 6.26

FC08-C06-U030 · Ch. 6, § Smooth Approximation of Maps Between Manifolds; source L3855 · not formalized

Theorem 6.26 (Whitney Approximation Theorem). Suppose N is a smooth manifold with or without boundary, M is a smooth manifold (without boundary), and $F \colon N \to M$ is a continuous map. Then F is homotopic to a smooth map. If F is already smooth on a closed subset $A \subseteq N$ , then the homotopy can be taken to be relative we know that there are not.

Not formalized. none; no complete checked declaration under strict bundle semantics — SmoothApprox.lean approximates maps into normed vector spaces, not arbitrary manifold codomains, and provides no homotopy conclusion. The checked sources therefore do not own Lee’s manifold-valued Whitney approximation or its smooth-map extension corollary. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unfinished/sorry-dependent sources, isolated ingredients, and reconstruction of the substantive source theorem.

Corollary 6.27

FC08-C06-U031 · Ch. 6, § Smooth Approximation of Maps Between Manifolds; source L3873 · not formalized

(Extension Lemma for Smooth Maps). Suppose $N$ is a smooth manifold with or without boundary, $M$ is a smooth manifold, $A \subseteq N$ is a closed subset, and $f \colon A \to M$ is a smooth map. Then $f$ has a smooth extension to $N$ if and only if it has a continuous extension to $N$.

Definition/convention — smooth homotopy

FC08-C06-U032 · Ch. 6, § Smooth Approximation of Maps Between Manifolds; source L3880 · not formalized

Lemma 6.28 If N and M are two smooth manifolds with or without boundary, a homotopy $H \colon N \times I \to M$ is called a smooth homotopy if it is also a smooth map, in the sense that it extends to a smooth map on some neighborhood of $N \times I \mathrm { ~ i n ~ } N \times \mathbb { R } .$ . Two maps are said to be smoothly homotopic if there is a smooth homotop Given any positive continuous function ı M R, there exists a smooth function $\widetilde { F } \colon M \to \overline { { \mathbb { R } } } ^ { k }$ that is ı-close to F .

Not formalized. none; no complete checked declaration under strict bundle semantics — Topology has homotopy infrastructure and manifold calculus has ContMDiff, but P/H define no smooth-homotopy object/relation with Lee’s neighborhood-of-N×I extension semantics, nor the equivalence/homotopic-implies-smoothly-homotopic theorems. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unfinished/sorry-dependent sources, isolated ingredients, and reconstruction of the substantive source theorem.

Lemma 6.28

FC08-C06-U033 · Ch. 6, § Smooth Approximation of Maps Between Manifolds; source L3882 · not formalized

Lemma 6.28. If N and M are smooth manifolds with or without boundary, smooth homotopy is an equivalence relation on the set of all smooth maps from N to M . P

Theorem 6.29

FC08-C06-U034 · Ch. 6, § Smooth Approximation of Maps Between Manifolds; source L3892 · not formalized

Theorem 6.29. Suppose N is a smooth manifold with or without boundary, M is a smooth manifold, and F; $G \colon N \to M$ are smooth maps. If F and G are homotopic, then they are smoothly homotopic. If F and G are homotopic relative to some closed subset $A \subseteq N$ , then they are smoothly homotopic relative .

Definition/convention — source terminology/construction

FC08-C06-U035 · Ch. 6, § Transversality; source L3914 · not formalized

For many purposes, it is more convenient to work with the following more general definition. If $F \colon N \to M$ is a smooth map and $S \subseteq M$ is an embedded submanifold, we say that F is transverse to S if for every $x \in F ^ { - 1 } ( S )$ the spaces $T _ { F ( x ) } S$ and d $F _ { x } ( T _ { x } N )$ together span $T _ { F ( x ) } M$ . One special case is worth noting: if F is a smooth submersion, then it is automatically transverse to every embedded submanifold of M . Two embedded submanifolds intersect transversely if and only if the inclusion of either one is transverse to the other.

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked P/H transversality predicate or theorem package exists. Bordism.lean only mentions transversality in comments, while targeted searches find no parametric transversality or transversality-homotopy implementation. These rows also depend on the missing general embedded-submanifold abstraction from C05. Strict bundle semantics reject proper subsets, stronger-hypothesis substitutes, unfinished/sorry-dependent sources, isolated ingredients, and reconstruction of the substantive source theorem.

Theorem 6.30

FC08-C06-U036 · Ch. 6, § Transversality; source L3918 · not formalized

Suppose $N$ and $M$ are smooth manifolds and $S \subseteq M$ is an embedded submanifold. (a) If $F \colon N \to M$ is a smooth map transverse to $S$, then $F^{-1}(S)$ is an embedded submanifold of $N$ whose codimension equals the codimension of $S$ in $M$. (b) If $S' \subseteq M$ is an embedded submanifold intersecting $S$ transversely, then $S \cap S'$ is an embedded submanifold of $M$ whose codimension is the sum of the codimensions of $S$ and $S'$.

Corollary 6.31

FC08-C06-U037 · Ch. 6, § Transversality; source L3940 · not formalized

Corollary 6.31. Suppose N and M are smooth manifolds, $S \subseteq M$ is an embedded submanifold of codimension k, and $F \colon N \to M$ is a submersion. Then $F ^ { - 1 } ( S )$ is an embedded codimension-k submanifold t for NM in $\mathbb { R } ^ { n } \times \mathbb { R } ^ { n }$ Fig.

Theorem 6.32

FC08-C06-U038 · Ch. 6, § Transversality; source L3944 · not formalized

Theorem 6.32 (Global Characterization of Graphs). Suppose M and N are smooth manifolds and $S \subseteq M \times N$ is an immersed submanifold. Let and denote the projections from $M \times N$ onto M and N , respectively. The following are equivalent. (a) S is the graph of a smooth map $f \colon M \to N .$ (b) $\pi _ { M } | _ { S }$ is a diffeomorphism from S onto $M .$ (c) For each $p \in M ,$ the submanifolds S and $\{ p \} \times N$ intersect transversely in exactly one point. If these conditions hold, then S is the graph of the map $f \colon M \to N$ defined by $\dot { \boldsymbol { f } } = \pi _ { N } \circ ( \pi _ { M } | _ { S } ) ^ { - 1 }$

Corollary 6.33

FC08-C06-U039 · Ch. 6, § Transversality; source L3956 · not formalized

Corollary 6.33 (Local Characterization of Graphs). Suppose M and N are smooth manifolds, $S \subseteq M \times N$ is an immersed submanifold, and $( p , q ) \in S$ . If S intersects the submanifold $\{ p \} \times N$ transversely at $( p , q )$ , then there exist a neighborhood U of p in M and a neighborhood V of $( p , q )$ in S such that V is the graph of a smooth map $f \colon U \to N$

Definition/convention — smooth family vertof maps

FC08-C06-U040 · Ch. 6, § Transversality; source L3962 · not formalized

Suppose N , M; and S are smooth manifolds, and for each $s \in S$ we are given a map $F _ { s } \colon N \to M$ The collection $\{ F _ { s } : s \in S \}$ is called a smooth family $\vert o f$ maps if the map $F \colon M \times S N$ defined by $F ( x , s ) = F _ { s } ( x )$ is smooth. You should think of such a family as a higher-dimensional analogue of a homotopy. The next proposition shows how such families are related to ordinary hom feomorphism on a neighborhood of $( x , 0 )$ in NM; which we can take to be of the form $V _ { \delta } ( x ) = \{ ( x ^ { \prime } , v ^ { \prime } ) \in N M : | x - x ^ { \prime } | < \delta$ ; v < ı for some $\delta > 0$ .

Proposition 6.34

FC08-C06-U041 · Ch. 6, § Transversality; source L3964 · not formalized

Proposition 6.34. If $\{ F _ { s } : s \in S \}$ is a smooth family of maps from N to M and S is connected, then for any $s _ { 1 } , s _ { 2 } \in S$ , the maps $F _ { s _ { 1 } } , F _ { s _ { 2 } } \colon N M$ are homotopic.

Definition/convention — family of smooth maps to contain at least one map that

FC08-C06-U042 · Ch. 6, § Transversality; source L3968 · not formalized

The key to finding transverse maps is an application of Sard’s theorem giving a sufficient condition for a family of smooth maps to contain one transverse to a given submanifold. If $S$ is a smooth manifold and $B \subseteq S$ is a subset whose complement has measure zero in $S$, we say $B$ contains almost every element of $S$.

Theorem 6.35

FC08-C06-U043 · Ch. 6, § Transversality; source L3970 · not formalized

Theorem 6.35 (Parametric Transversality Theorem). Suppose N and M are smooth manifolds, $X \subseteq M$ is an embedded submanifold, and $\{ F _ { s } : s \in S \}$ is a smooth family of maps from N to M . If the map $F \colon N \times S \to M$ is transverse to X, then for almost every $s \in S$ , the map $F _ { s } \colon N \to M$ is transverse to $X$.

Theorem 6.36

FC08-C06-U044 · Ch. 6, § Transversality; source L4014 · not formalized

Theorem 6.36 (Transversality Homotopy Theorem). Suppose M and N are smooth manifolds and $X \subseteq M$ is an embedded submanifold. Every smooth map $f \colon N \to$ M is homotopic to a smooth map g $N M$ that is transverse ote that $E ( x , 0 ) = x$ , so $r ( x ) = \pi \circ E ^ { - 1 } ( x ) = \pi ( x , 0 ) = x$ , which shows that r is a retraction.