FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013)
FC08 — Lee, Introduction to Smooth Manifolds.
This chapter contains 16 definitions, 4 theorems, 8 propositions, 4 lemmas, 1 corollary and 2 examples.
Of the 35 statements checked against Lean, 22 are formalized somewhere and 13 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 22 | 63% | Mathlib states and proves it. |
| not formalized | 13 | 37% | A documented search found no Lean statement of it anywhere. |
| checked in total | 35 |
- Canonical source block: FC08 Lee, Chapter 2,
FC08-C02-U001–FC08-C02-U035, exactly 35 unique contiguous rows retrieved from FC08 — John M. Lee, Introduction to Smooth Manifolds throughagent-memory. - Search order followed the Sweep-II plan: project source first at
A=3b2239e161592472b34e02ad3b7da308f9ce7280, then pinned MathlibP=db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean 4.33.0), current upstream MathlibH=5315eef9e4ffb98e0f89f278b765c50a149f66ca(Apache-2.0, Lean 4.34.0-rc2), current/open/indexed searches, Reservoir and broad discoverable Lean sources, then local reference mirrors. Noproject-existing,package-import, orreference-portC02 owner survived strict bundle checking. - Every promoted path exists at exact
P, and the promoted declaration set compiled through the project toolchain./tmp/fc08-c02-witness.leanadditionally compiled exact audit witnesses for U009 (smooth gluing over an arbitrary open cover), U022 (arbitrary two-threshold cutoff), U024 (radial Euclidean bump with the strict annular inequalities), U031 (closed-set bump withtsupportinside the prescribed open set), and U035 (closed set as an exact smooth zero locus). These witnesses only assemble pinned Mathlib declarations; they are audit evidence, not project source. - C02 has 22 pinned
mathlibrows and 13 datedunmatchedrows. Positive rows are: U002, U003, U004, U005, U006, U007, U008, U009, U010, U011, U012, U016, U017, U021, U022, U024, U026, U027, U028, U029, U031, U035. - Smooth-map rows U002–U012 are mapped through Mathlib’s charted-manifold
ContMDiffinterface rather than by name analogy. Extended charts/model-with-corners encode Lee’s boundary convention; maximal-atlas lemmas give chart independence; open-subtype and open-union lemmas supply locality and the gluing assembly. - U017 is exact in both parts:
OpenPartialHomeomorph.univUnitBalluses Lee’s explicit inverse square-root formulas and is proved smooth in both directions, whileOpenPartialHomeomorph.toStructomorphturns every smooth atlas chart into a smooth diffeomorphism between its open source and target. - U018 and U020 are deliberately not promoted. Mathlib proves most of U018 and proves
Diffeomorph.image_boundary/image_interiorfor U020, but the checked pin has no complete packaged restriction-to-an-open-submanifold/interior diffeomorphism interface closing the remaining clauses. Whole-row semantics reject those partial matches. - U024 is not credited merely from
ContDiffBump: that interface guarantees 1 on the inner closed ball and positivity in the outer ball but does not guarantee strict< 1throughout the annulus (its base file explicitly does not assume an iff characterization of the one-locus). The promoted route instead usesReal.smoothTransitioncomposed with squared norm, and the audit witness checks all strict inequalities. - U028 uses
PartitionOfUnity.IsSubordinate, which is defined withtsupport, i.e. closure of nonzero support, exactly matching Lee’s support convention;locallyFinite_tsupportalso proves local finiteness for those closed supports. U029 is then the direct smooth subordinate-partition existence theorem under the standard Lee manifold hypotheses. - U031 is a short exact corollary of U029 using the two-set cover
U, Aᶜ; the pinned witness verifies smoothness,[0,1]bounds, equality to 1 onA, andtsupport ⊆ U. - U033 is not inferred from Tietze extension or
Continuous.exists_contMDiff_approx_and_eqOn: the latter starts with an ambient continuous function already smooth on a neighborhood of the closed set, while Lee starts only with a map defined on the closed subset that is locally extendable. Turning those ingredients into Lee’s global support-controlled extension is the substantive theorem itself. - U034 remains unmatched after pinned/current/external search: no checked positive smooth exhaustion-function theorem was found. U035 is direct from
exists_contMDiff_zero_iff_one_iff_of_isClosedwith the second closed set specialized to∅. - Current upstream
H=5315eef9e4ffb98e0f89f278b765c50a149f66cawas fetched as an object only (no checkout); itslean-toolchainis Lean 4.34.0-rc2, and the C02 gap probes did not reveal a current-only owner for U033 or U034. The pinned Mathlib worktree remained clean. N=2026-09-07denotes a dated unmatched result after the prescribed search layers. Strict whole-row semantics apply uniformly.
Definition/convention — map
Although the terms function and map are technically synonymous, in studying smooth manifolds it is often convenient to make a slight distinction between them. Throughout this book we generally reserve the term function for a map whose codomain is R (a real-valued function) or \(\mathbb { R } ^ { k }\) for some \(k > 1\) (a vector-valued function). Either of the words map or mapping can mean any type of map, such as a map between arbitrary manifolds. ##
Not formalized. none; no complete checked declaration under strict bundle semantics — This is Lee-specific prose distinguishing “function” from “map”; Lean has no corresponding mathematical interface to own the terminology convention. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Definition/convention — source terminology/construction
Suppose M is a smooth n-manifold, k is a nonnegative integer, and \(f \colon M \to \mathbb { R } ^ { k }\) is any function. We say that f is a smooth function if for every \(p \in M\) ; there exists a smooth chart \(( U , \varphi )\) for M whose domain contains p and such that the composite function \(f \circ \varphi ^ { - 1 }\) is smooth on the open subset \({ \widehat { U } } = \varphi ( U ) \subseteq \mathbb { R } ^ { n } { \mathrm { ~ ( F i g . ~ } } 2 . 1 )\) If M is a smooth manifold with boundary, the definition is exactly the same, except that \(\varphi ( U )\) is now an open subset of either \(\mathbb { R } ^ { n }\) or \(\mathbb { H } ^ { n }\) , and in the latter case we interpret smoothness of \(f \circ \varphi ^ { - 1 }\) to mean that each point of \(\varphi ( U )\) has a neighborhood \(( \mathrm { i n } \mathbb { R } ^ { n } )\) on which \(f \circ \varphi ^ { - 1 }\)
Formalized. Mathlib/Geometry/Manifold/ContMDiff/Defs.lean::ContMDiff, contMDiff_iff; Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean::OpenPartialHomeomorph.contMDiffOn_writtenInExtend_iff — ContMDiff is the manifold-smoothness predicate. contMDiff_iff characterizes it by continuity plus smooth coordinate expressions, and the written-in-extended-chart theorem specializes this to real/vector-valued functions, including models with boundary.
Definition/convention — source terminology/construction
The most important special case is that of smooth real-valued functions \(f \colon M \to\) R; the set of all such functions is denoted by \(C ^ { \infty } ( M )\) . Because sums and constant multiples of smooth functions are smooth, \(C ^ { \infty } ( M )\) is a vector space under pointwise addition and multiplication by constants.
Formalized. Mathlib/Geometry/Manifold/ContMDiffMap.lean::ContMDiffMap; Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean::ContMDiffMap.module — ContMDiffMap I M 𝓘(ℝ) ℝ ∞ is the bundled space of smooth real-valued functions, and the module instance gives closure under addition and real scalar multiplication, exactly Lee’s C^∞(M) vector-space assertion.
Definition/convention — coordinate representation of f
Given a function \(f \colon M \to \mathbb { R } ^ { k }\) and a chart \(( U , \varphi )\) for M; the function \({ \widehat { f } } \colon \varphi ( U ) \to \mathbb { R } ^ { k }\) defined by \({ \hat { f } } ( x ) = f \circ \varphi ^ { - 1 } ( x )\) is called the coordinate representation of f . By definition, f is smooth if and only if its coordinate representation is smooth in some smooth chart around each point. By the preceding exercise, smooth functions have smooth coordinate representat ures was to enable us to define smooth functions on manifolds and smooth maps between manifolds.
Formalized. Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean::OpenPartialHomeomorph.contMDiffOn_writtenInExtend_iff, IsManifold.mem_maximalAtlas_iff_contMDiffOn; Mathlib/Geometry/Manifold/ContMDiff/Defs.lean::contMDiff_iff — Mathlib writes the coordinate representation as the target chart composed with f and the inverse source chart (using extended charts for corners). Membership in the maximal smooth atlas makes the criterion independent of the chosen smooth chart, matching both “some chart” and “every smooth chart” clauses.
Definition/convention — map
The definition of smooth functions generalizes easily to maps between manifolds. Let M; N be smooth manifolds, and let \(F \colon M \to N\) be any map. We say that F is a smooth map if for every \(p \in M\) ; there exist smooth charts \(( U , \varphi )\) containing p and .V; / containing \(F ( p )\) such that \(F ( U ) \subseteq V\) and the composite map \(F \circ\) \(\varphi ^ { - 1 }\) is smooth from \(\varphi ( U )\) to .V / (Fig. 2.2). If M and N are smooth manifolds with boundary, smoothness of F is defined in exactly the same way, with the usual understanding that a map whose domain is a subset of \(\mathbb { H } ^ { n }\) is smooth if it admits an extension to a smooth map in a neighborhood of each point, and a map whose codomain is a subset of \(\mathbb { H } ^ { n }\) is smooth if it is smooth as a map into \(\mathbb { R } ^ { n }\) . Note that our previous definition of smoothness of real-valued or vector-valued functions can be viewed as a special case of this one, by taking \(N = V = \mathbb { R } ^ { k }\) and \(\psi = \mathrm { I d } \colon \mathbb { R } ^ { k } \to \mathbb { R } ^ { k }\)
Formalized. Mathlib/Geometry/Manifold/ContMDiff/Defs.lean::ContMDiff, contMDiff_iff, contMDiffAt_iff_of_mem_maximalAtlas — ContMDiff I I′ ∞ F is defined for maps between manifolds with arbitrary models with corners. Its chart characterization is exactly smoothness of the coordinate composite, including half-space/corner models through the model embeddings.
Proposition 2.4
Every smooth map is continuous.
Formalized. Mathlib/Geometry/Manifold/ContMDiff/Defs.lean::ContMDiff.continuous — Direct theorem: every ContMDiff map is continuous.
Proposition 2.5
(Equivalent Characterizations of Smoothness). Suppose \(M\) and \(N\) are smooth manifolds with or without boundary and \(F \colon M \to N\) is a map. Then \(F\) is smooth if and only if either of the following holds. (a) For every \(p \in M\) there exist smooth charts \((U,\varphi)\) containing \(p\) and \((V,\psi)\) containing \(F(p)\) such that \(U \cap F^{-1}(V)\) is open in \(M\) and the composite \(\psi \circ F \circ \varphi^{-1}\) is smooth from \(\varphi(U \cap F^{-1}(V))\) to \(\psi(V)\). (b) \(F\) is continuous and there exist smooth atlases \(\{(U_{\alpha},\varphi_{\alpha})\}\) and \(\{(V_{\beta},\psi_{\beta})\}\) for \(M\) and \(N\) such that for each \(\alpha\) and \(\beta\), \(\psi_{\beta} \circ F \circ \varphi_{\alpha}^{-1}\) is a smooth map from \(\varphi_{\alpha}(U_{\alpha} \cap F^{-1}(V_{\beta}))\) to \(\psi_{\beta}(V_{\beta})\).
Formalized. Mathlib/Geometry/Manifold/ContMDiff/Defs.lean::contMDiff_iff, contMDiffAt_iff_of_mem_maximalAtlas; Mathlib/Geometry/Manifold/IsManifold/Basic.lean::IsManifold.subset_maximalAtlas — contMDiff_iff gives continuity plus chartwise smoothness, while contMDiffAt_iff_of_mem_maximalAtlas permits arbitrary charts in the maximal smooth atlases. Atlas charts lie in that maximal atlas, yielding Lee’s two equivalent chart/atlas formulations.
Proposition 2.6
Proposition 2.6 (Smoothness Is Local). Let M and N be smooth manifolds with or without boundary, and let \(F \colon M \to N\) be a map. (a) If every point \(p \in M\) has a neighborhood U such that the restriction \(F | _ { U }\) is smooth, then F is smooth. (b) Conversely, if F is smooth, then its restriction to every open subset is smoo een \(\hat { f }\) and \(f\) itself, and instead say something like \(^ { 6 6 } f\) is smooth on \(U\) because its coordinate representation \(f ( r , \theta ) = r ^ { 2 }\) is smooth.” Fig.
Formalized. Mathlib/Geometry/Manifold/ContMDiff/Defs.lean::ContMDiff.contMDiffOn, contMDiff_of_locally_contMDiffOn; Mathlib/Geometry/Manifold/ContMDiff/Basic.lean::ContMDiffOn.iUnion_of_isOpen, contMDiff_of_contMDiffOn_iUnion_of_isOpen — ContMDiff.contMDiffOn gives restriction to any subset, and contMDiff_of_locally_contMDiffOn/the open-union theorem recover global smoothness from smoothness on neighborhoods. This is exactly the two directions of smoothness being local.
Corollary 2.8
Corollary 2.8 (Gluing Lemma for Smooth Maps). Let M and N be smooth manifolds with or without boundary, and let \(\{ U _ { \alpha } \} _ { \alpha \in A }\) A .$ , we are given a smooth map \(F _ { \alpha } \colon U _ { \alpha } \to N\) such that the maps agree on overlaps: \(F _ { \alpha } | _ { U _ { \alpha \cap U _ { \beta } } = F _ { \beta } | _ { U _ { \alpha \cap U _ { \beta } }\) for all ˛ and ˇ. Then there exists a unique smooth map \(F \colon M \to N\) such that \(F | _ { U _ { \alpha } } = F _ { \alpha }\) for each ˛ $
Formalized. Mathlib/Geometry/Manifold/ContMDiff/Basic.lean::contMDiffAt_subtype_iff, ContMDiffOn.iUnion_of_isOpen, contMDiff_of_contMDiffOn_iUnion_of_isOpen; Mathlib/Geometry/Manifold/ContMDiff/Defs.lean::ContMDiff.congr — The pinned APIs prove the exact gluing lemma: compatible local maps define a unique set-theoretic global map; contMDiffAt_subtype_iff transfers each local smooth map from its open subtype, ContMDiff.congr identifies it with the glued map there, and the open-union theorem proves global smoothness. This complete assembly was compiled in the C02 audit witness.
Definition/convention — source terminology/construction
\(F \colon M \to N\) is a smooth map, and \(( U , \varphi )\) and \(( V , \psi )\) are any smooth charts for M and N , respectively, we call \(\widehat { F } = \psi \circ F \circ \varphi ^ { - 1 }\) the coordinate representation of F with respect to the given coordinates. It maps the set \(\varphi \big ( U \cap F ^ { - 1 } ( V ) \big )\) to \(\psi ( V )\)
Formalized. Mathlib/Geometry/Manifold/ContMDiff/Defs.lean::contMDiffWithinAt_iff_of_mem_maximalAtlas, contMDiffOn_iff_of_mem_maximalAtlas; Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean::ModelWithCorners.extendCoordChange — The formal coordinate expression is the target extended chart composed with F and the inverse source extended chart on the relevant overlap. These theorems expose exactly that representation for arbitrary smooth charts.
Proposition 2.10
Proposition 2.10. Let M; N; and P be smooth manifolds with or without boundary. (a) Every constant map c \(M \to N\) is smooth. (b) The identity map of M is smooth. (c) If \(U \subseteq M\) is an open submanifold with or without boundary, then the inclusion map \(U \hookrightarrow M\) is smooth. (d) If \(F \colon M \to N\) and \(G \colon N \to P\) are smooth, then s
Formalized. Mathlib/Geometry/Manifold/ContMDiff/Basic.lean::contMDiff_const, contMDiff_id, contMDiff_subtype_val, ContMDiff.comp — The four cited declarations are respectively Lee’s constant-map, identity-map, open-submanifold inclusion, and composition clauses.
Proposition 2.12
Exercise 2.11. Prove parts (a)–(c) of the preceding proposition. Proposition 2.12. Suppose \(M _ { 1 } , \ldots , M _ { k }\) and N are smooth manifolds with or without boundary, such that at most one of \(M _ { 1 } , \dots , M _ { k }\) has nonempty boundary. For each i, let \(\pi _ { i } \colon M _ { 1 } \times \cdots \times M _ { k } \to M _ { i }\) denote the projection onto the \(M _ { i }\) factor. A map \(F \colon N \to M _ { 1 } \times \cdots \times M _ { k }\) is smooth if and only if each of the component maps \(F _ { i } = \pi _ { i } \circ F \colon N \to M _ { i }\)
Formalized. Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean::contMDiff_fst, contMDiff_snd, contMDiff_prod_iff; Mathlib/Geometry/Manifold/IsManifold/Basic.lean::IsManifold.prod — contMDiff_prod_iff says a map into a binary product is smooth iff both components are smooth; iteration gives the finite product. Mathlib’s product model with corners is stronger than Lee’s “at most one boundary factor” restriction.
Definition/convention — source terminology/construction
Although most of our efforts in this book are devoted to the study of smooth manifolds and smooth maps, we also need to work with topological manifolds and continuous maps on occasion. For the sake of consistency, we adopt the following conventions: without further qualification, the words “function” and “map” are to be understood purely in the set-theoretic sense, and carry no assumptions of continuity or smoothness. Most other objects we study, however, will be understood to carry some minimal topological structure by default. Unless otherwise specified, a “manifold” or “manifold with boundary” is always to be understood as a topological one, and a “coordinate chart” is to be understood in the topological sense, as a homeomorphism from an open subset of the manifold to an open subset of \(\mathbb { R } ^ { n }\) or \(\mathbb { H } ^ { n }\) . If we wish to restrict attention to smooth manifolds or smooth coordinate charts, we will say so. Similarly, our default assumptions for many other specific types of geometric objects and the maps between them will be continuity at most; smoothness will not be assumed unless explicitly specified. The only exceptions will be a few concepts that require smoothness for their very definition.
Not formalized. none; no complete checked declaration under strict bundle semantics — This is a book-wide default-language convention about the unqualified words “map”, “manifold”, and “chart”, not a Lean mathematical declaration. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Definition/convention — source terminology/construction
On the other hand, because the definition of a smooth map requires smooth structures in the domain and codomain, if we say “F M N is a smooth map” without specifying what M and N are, it should always be understood that they are smooth manifolds with or without boundaries. W
Not formalized. none; no complete checked declaration under strict bundle semantics — This is another source-language convention about omitted type assumptions, not a mathematical interface. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Example 2.13
Example 2.13 (Smooth Maps). (a) Any map from a zero-dimensional manifold into a smooth manifold with or without boundary is automatically smooth, because each coordinate representation is constant. (b) If the circle \(\mathbb { S } ^ { 1 }\) is given its standard smooth structure, the map \(\varepsilon \colon \mathbb { R } \to \mathbb { S } ^ { 1 }\) defined by \(\varepsilon ( t ) = e ^ { 2 \pi i t }\) is smooth, because with respect to any angle coordinate for \(\mathbb { S } ^ { 1 }\) (see Problem 1-8) it has a coordinate representation of the form \(\widehat { \varepsilon } ( t ) = 2 \pi t + c\) for some constant c, as you can check. (c) The map \(\varepsilon ^ { n } \colon \mathbb { R } ^ { n } \to \mathbb { T } ^ { n }\) defined by \(\varepsilon ^ { n } ( x ^ { 1 } , \ldots , x ^ { n } ) = \left( e ^ { 2 \pi i x ^ { 1 } } , \ldots , e ^ { 2 \pi i x ^ { n } } \right)\) is smooth by Proposition 2.12. (d) Now consider the n-sphere \(\mathbb { S } ^ { n }\) with its standard smooth structure. The inclusion map \(\iota \colon \mathbb { S } ^ { n } \hookrightarrow \mathbb { R } ^ { n + 1 }\) is certainly continuous, because it is the inclusion map of a topological subspace. It is a smooth map because its coordinate representation with respect to any of the graph coordinates of Example 1.31 is \[ \begin{array}{r l} & {\widehat {\iota} (u ^ {1}, \ldots , u ^ {n}) = \iota \circ (\varphi_ {i} ^ {\pm}) ^ {- 1} (u ^ {1}, \ldots , u ^ {n})} \\ & {\qquad = (u ^ {1}, \ldots , u ^ {i - 1}, \pm \sqrt {1 - | u | ^ {2}}, u ^ {i}, \ldots , u ^ {n}),} \end{array} \] which is smooth on its domain (the set where \(| u | ^ { 2 } < 1 )\) . (e) The quotient map \(\pi \colon \mathbb { R } ^ { n + 1 } \setminus \{ 0 \} \to \mathbb { R P } ^ { n }\) used to define \(\mathbb { R P } ^ { n }\) is smooth, because its coordinate representation in terms of any of the coordinates for \(\mathbb { R P } ^ { n }\) constructed in Example 1.33 and standard coordinates on \(\mathbb { R } ^ { n + 1 } \setminus \{ 0 \}\) is \[ \begin{array}{c} \hat {\pi} \left(x ^ {1}, \ldots , x ^ {n + 1}\right) = \varphi_ {i} \circ \pi \left(x ^ {1}, \ldots , x ^ {n + 1}\right) = \varphi_ {i} \left[ x ^ {1}, \ldots , x ^ {n + 1} \right] \\ = \left(\frac {x ^ {1}}{x ^ {i}}, \ldots , \frac {x ^ {i - 1}}{x ^ {i}}, \frac {x ^ {i + 1}}{x ^ {i}}, \ldots , \frac {x ^ {n + 1}}{x ^ {i}}\right). \end{array} \] (f) Define \(q \colon \mathbb { S } ^ { n } \to \mathbb { R P } ^ { n }\) as the restriction of \(\pi \colon \mathbb { R } ^ { n + 1 } \setminus \{ 0 \} \to \mathbb { R P } ^ { n }\) to \(\mathbb { S } ^ { n } \subseteq\) R \(\mathit { n } ^ { + 1 } \setminus \{ 0 \}\) . It is a smooth map, because it is the composition \(q = \pi \circ \iota\) of the maps in the preceding two examples. (g) If \(M _ { 1 } , \dots , M _ { k }\) are smooth manifolds, then each projection map \(\pi _ { i } \colon M _ { 1 } \times \cdots \times\) \(M _ { k } \to M _ { i }\) is smooth, because its coordinate representation with respect to any of the product charts of Example 1.8 is just a coordinate projection. ## Diffeomorphisms If M and N are smooth manifolds with or without boundary, a diffeomorphism from M to N is a smooth bijective of geometric objects and the maps between them will be continuity at most; smoothness will not be assumed unless explicitly specified.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib owns several clauses (smooth sphere inclusion, product projections, and generic smooth-map composition) but no checked real-projective-space smooth manifold/quotient package realizes the full seven-part example. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Definition/convention — diffeomorphism
If \(M\) and \(N\) are smooth manifolds with or without boundary, a diffeomorphism from \(M\) to \(N\) is a smooth bijective map \(F \colon M \to N\) with a smooth inverse. \(M\) and \(N\) are diffeomorphic, written \(M \approx N\), if such a map exists.
Formalized. Mathlib/Geometry/Manifold/Diffeomorph.lean::Diffeomorph — Diffeomorph I I′ M N ∞ extends an equivalence by smoothness of the forward and inverse maps, exactly Lee’s definition.
Example 2.14
(Diffeomorphisms). (a) The maps \(F \colon \mathbb{B}^{n} \to \mathbb{R}^{n}\) and \(G \colon \mathbb{R}^{n} \to \mathbb{B}^{n}\) given by \[ F(x) = \frac{x}{\sqrt{1 - |x|^{2}}}, \qquad G(y) = \frac{y}{\sqrt{1 + |y|^{2}}} \tag{2.1} \] are smooth and mutually inverse, so both are diffeomorphisms and \(\mathbb{B}^{n}\) is diffeomorphic to \(\mathbb{R}^{n}\). (b) If \(M\) is a smooth manifold and \((U,\varphi)\) is a smooth chart on \(M\), then \(\varphi \colon U \to \varphi(U) \subseteq \mathbb{R}^{n}\) is a diffeomorphism, its coordinate representation being the identity.
Formalized. Mathlib/Analysis/Normed/Module/Ball/Homeomorph.lean::OpenPartialHomeomorph.univUnitBall, Homeomorph.unitBall; Mathlib/Analysis/InnerProductSpace/Calculus.lean::OpenPartialHomeomorph.contDiff_univUnitBall, OpenPartialHomeomorph.contDiffOn_univUnitBall_symm; Mathlib/Geometry/Manifold/HasGroupoid.lean::OpenPartialHomeomorph.toStructomorph — univUnitBall is exactly the homeomorphism y ↦ y/√(1+‖y‖²) from Euclidean space onto the unit ball, with inverse x ↦ x/√(1-‖x‖²), and both directions are smooth. Separately, every chart in a smooth atlas becomes a smooth Structomorph between its open source and target, which is Lee’s chart-is-a-diffeomorphism clause.
Proposition 2.15
map as a coordinate representation.) ## Proposition 2.15 (Properties of Diffeomorphisms). (a) Every composition of diffeomorphisms is a diffeomorphism. (b) Every finite product of diffeomorphisms between smooth manifolds is a diffeomorphism. (c) Every diffeomorphism is a homeomorphism and an open map. (d) The restriction of a diffeomorphism to an open submanifold with or without boundary is a diffeomorphism onto its image. (e) “Diffeomorphic” is an equivalence relation on the class of all smooth manifolds with or without boundary. E
Not formalized. none; no complete checked declaration under strict bundle semantics — Diffeomorph.refl/symm/trans/prodCongr, toHomeomorph, and local-diffeomorphism openness cover most clauses, but no checked declaration packages the restriction of an arbitrary diffeomorphism to an arbitrary open submanifold as a diffeomorphism onto its image. Strict bundle semantics therefore reject the partial match. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Theorem 2.17
Theorem 2.17 (Diffeomorphism Invariance of Dimension). A nonempty smooth manifold of dimension m cannot be diffeomorphic to an n-dimensional smooth manifold unless m n.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem identifies dimensions of nonempty finite-dimensional real manifolds from existence of a diffeomorphism. Diffeomorphism and finite-dimensional manifold APIs are adjacent but do not supply Lee’s invariance-of-dimension conclusion. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Theorem 2.18
Theorem 2.18 (Diffeomorphism Invariance of the Boundary). Suppose M and N are smooth manifolds with boundary and F \(M \to N\) is a diffeomorphism. Then \(F ( \partial M ) = \partial N\) , and F restricts to a diffeomorphism from Int M to Int
Not formalized. none; no complete checked declaration under strict bundle semantics — Diffeomorph.image_boundary and Diffeomorph.image_interior prove the image equalities, but no checked declaration packages the induced restriction Int M → Int N as a Diffeomorph; the complete two-clause theorem is therefore not promoted. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Lemma 2.20
Lemma 2.20. The function f R R defined by \[ f (t) = \left\{ \begin{array}{l l} e ^ {- 1 / t}, & t > 0, \\ 0, & t \leq 0, \end{array} \right. \]
Formalized. Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean::expNegInvGlue, expNegInvGlue.zero_of_nonpos, expNegInvGlue.pos_of_pos, expNegInvGlue.contDiff — expNegInvGlue is literally Lee’s piecewise function exp (-1/t) for t>0 and 0 for t≤0, and Mathlib proves it infinitely smooth.
Lemma 2.21
Lemma 2.21. Given any real numbers \(r _ { 1 }\) and \(r _ { 2 }\) such that \(r _ { 1 } < r _ { 2 }\) , there exists a smooth function \(h \colon { \mathbb { R } } \to { \mathbb { R } }\) such that \(h ( t ) \equiv 1 \mathrm { ~ } f o r \mathrm { ~ } t \mathrm { ~ } \le r _ { 1 } , 0 < h ( t ) < 1 \mathrm { ~ } f o r \mathrm { ~ } r _ { 1 } <\) \(t < r _ { 2 }\) , and \(h ( t ) \equiv 0 f o r t \geq r _ { 2 }\)
Formalized. Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean::Real.smoothTransition, Real.smoothTransition.zero_of_nonpos, Real.smoothTransition.one_of_one_le, Real.smoothTransition.pos_of_pos, Real.smoothTransition.lt_one_of_lt_one, Real.smoothTransition.contDiff — After the affine rescaling (t-r₁)/(r₂-r₁) and replacing s by 1-s, Real.smoothTransition gives exactly Lee’s cutoff: 1 on the left, strictly between 0 and 1 in the transition interval, and 0 on the right. The arbitrary-r₁<r₂ assembly was compiled at P.
Definition/convention — cutoff function
A function with the properties of h in the preceding lemma is usually called a cutoff function.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has the concrete Real.smoothTransition used as a cutoff, but no checked CutoffFunction terminology/interface corresponding to Lee’s naming-only row. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Lemma 2.22
Given any positive real numbers \(r_{1} < r_{2}\), there is a smooth function \(H \colon \mathbb{R}^{n} \to \mathbb{R}\) with \(H \equiv 1\) on \(\overline{B}_{r_{1}}(0)\), \(0 < H(x) < 1\) for all \(x \in B_{r_{2}}(0) \setminus \overline{B}_{r_{1}}(0)\), and \(H \equiv 0\) on \(\mathbb{R}^{n} \setminus B_{r_{2}}(0)\).
Formalized. Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean::Real.smoothTransition; Mathlib/Analysis/InnerProductSpace/Calculus.lean::contDiff_norm_sq — Composing 1-smoothTransition with (‖x‖²-r₁²)/(r₂²-r₁²) gives Lee’s radial bump exactly: 1 on the closed inner ball, strictly between 0 and 1 on the annulus, and 0 outside the outer open ball. contDiff_norm_sq makes the radial parameter smooth at the origin; the complete inequalities and smoothness compiled at P.
Definition/convention — smooth real-valued function that
The function H constructed in this lemma is an example of a smooth bump function, a smooth real-valued function that is equal to 1 on a specified set and is zero outside a specified neighborhood of that set. Later in this chapter, we will generalize this notion to manifolds.
Not formalized. none; no complete checked declaration under strict bundle semantics — ContDiffBump is a bundled radial/centered bump and realizes the preceding Euclidean example, but it is a specialization of Lee’s generic “equal to 1 on a specified set and zero outside a specified neighborhood” notion; no general named predicate was found. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Definition/convention — source terminology/construction
If f is any real-valued or vector-valued function on a topological space M; the support of f , denoted by supp f , is the closure of the set of points where f is nonzero: \[ \operatorname{supp} f = \overline {{\left\{p \in M : f (p) \neq 0 \right\}}}. \]
Formalized. Mathlib/Topology/Algebra/Support.lean::tsupport — tsupport f is defined as closure (Function.support f), and additive support is the nonzero locus, exactly Lee’s support convention.
Definition/convention — compactly supported
(For example, if H is the function constructed in the preceding lemma, then supp \(H = \overline { { { B } } } _ { r _ { 2 } } ( 0 ) .\) ) If supp f is contained in some set \(U \subseteq M ,\) we say that f is supported in U . A function f is said to be compactly supported if supp f is a compact set. Clearly, every function on a compact space is compactly supported.
Formalized. Mathlib/Topology/Algebra/Support.lean::tsupport, HasCompactSupport, HasCompactSupport.of_compactSpace — HasCompactSupport f is compactness of tsupport f. Containment of tsupport expresses “supported in U”, and HasCompactSupport.of_compactSpace proves every function on a compact domain has compact support.
Definition/convention — partition of unity subordinate to mathcal X
The next construction is the most important application of paracompactness. Suppose M is a topological space, and let \(\mathcal { X } = ( X _ { \alpha } ) _ { \alpha \in A }\) be an arbitrary open cover of M; indexed by a set A. A partition of unity subordinate to \(\pmb { \mathcal X }\) is an indexed family \(( \psi _ { \alpha } ) _ { \alpha \in A }\) of continuous functions \(\psi _ { \alpha } \colon M \to \mathbb { R }\) with the following properties: (i) \(0 \leq \psi _ { \alpha } ( x ) \leq 1\) for all ˛ A and all \(x \in M .\) (ii) supp \(\psi _ { \alpha } \subseteq X _ { \alpha }\) for each \(\alpha \in A .\) (iii) The family of supports .supp \(\psi _ { \alpha } ) _ { \alpha \in A }\) is locally finite, meaning that every point has a neighborhood that intersects supp \(\psi _ { \alpha }\) for only finitely many values of \(\alpha .\) (iv) \(\textstyle \sum _ { { \boldsymbol { \alpha } } \in A } \psi _ { \boldsymbol { \alpha } } ( x ) = 1 { \mathrm { ~ f o r ~ a l l ~ } } x \in M .\) Because of the local finiteness condition (iii), the sum in (iv) actually has only finitely many nonzero terms in a neighborhood of each point, so there is no issue of convergence. If M is a smooth manifold with or without boundary, a smooth partition of unity is one for which each \(\psi_{\alpha}\) is smooth.
Formalized. Mathlib/Topology/PartitionOfUnity.lean::PartitionOfUnity, PartitionOfUnity.IsSubordinate, PartitionOfUnity.locallyFinite_tsupport, PartitionOfUnity.nonneg, PartitionOfUnity.le_one, PartitionOfUnity.sum_eq_one; Mathlib/Geometry/Manifold/PartitionOfUnity.lean::SmoothPartitionOfUnity — PartitionOfUnity bundles continuous nonnegative functions with locally finite support and pointwise sum 1; IsSubordinate is exactly tsupport (f i) ⊆ U i, and locallyFinite_tsupport upgrades the stored raw supports to Lee’s closed supports. SmoothPartitionOfUnity adds smoothness of every member.
Theorem 2.23
Theorem 2.23 (Existence of Partitions of Unity). Suppose M is a smooth manifold with or without boundary, and \(\mathcal { X } = ( X _ { \alpha } ) _ { \alpha \in A }\) is any indexed open cover of M . Then there exists a smooth partition of unity subordinate required form.
Formalized. Mathlib/Geometry/Manifold/PartitionOfUnity.lean::SmoothPartitionOfUnity.exists_isSubordinate; Mathlib/Topology/Compactness/SigmaCompact.lean::sigmaCompactSpace_of_locallyCompact_secondCountable; Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean::Manifold.locallyCompact_of_finiteDimensional — SmoothPartitionOfUnity.exists_isSubordinate is the exact existence theorem for an indexed open cover. Lee’s finite-dimensional second-countable Hausdorff manifold hypotheses supply Mathlib’s T2Space and SigmaCompactSpace assumptions via local compactness plus second countability.
Definition/convention — bump function for A supported in U
As our first application of partitions of unity, we extend the notion of bump functions to arbitrary closed subsets of manifolds. If M is a topological space, \(A \subseteq M\) M$ is an open subset containing A, a continuous function \(\psi \colon \to \mathbb { R }\) is called a bump function for A supported in U if $ $ on M; $ \mathrm {
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has all component notions (ContinuousMap, [0,1] bounds, EqOn, tsupport) and proves the existence theorem in U031, but no checked named predicate/structure owns Lee’s generic “bump function for A supported in U” definition as a first-class interface. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Proposition 2.25
Proposition 2.25 (Existence of Smooth Bump Functions). Let M be a smooth manifold with or without boundary. For any closed subset \(A \subseteq M\) and any open subset U containing A, there exists a smooth bump function for A supported suppose for this proof that M is a smooth manifold without boundary; the general case is left as an exercise.
Formalized. Mathlib/Geometry/Manifold/PartitionOfUnity.lean::SmoothPartitionOfUnity.exists_isSubordinate, SmoothPartitionOfUnity.IsSubordinate; Mathlib/Topology/PartitionOfUnity.lean::PartitionOfUnity.sum_eq_one, PartitionOfUnity.nonneg, PartitionOfUnity.le_one — Apply the smooth partition theorem to the two-set cover U, Aᶜ. The component subordinate to U has topological support inside U; the other component vanishes on A, so the sum-to-one law forces the first to equal 1 on A, with values in [0,1]. This exact closed-set bump theorem compiled in the C02 audit witness.
Definition/convention — there
Suppose \(M\) and \(N\) are smooth manifolds with or without boundary and \(A \subseteq M\) is an arbitrary subset. A map \(F \colon A \to N\) is smooth on \(A\) if it has a smooth extension in a neighborhood of each point: for every \(p \in A\) there is an open subset \(W \subseteq M\) containing \(p\) and a smooth map \(\widetilde{F} \colon W \to N\) whose restriction to \(W \cap A\) agrees with \(F\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has ContMDiffOn/ContMDiffWithinAt, but these mean differentiability of an ambiently defined map on a set, not Lee’s predicate for a map whose domain is only A and which locally extends off A. No checked equivalent interface was found. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Lemma 2.26
(Extension Lemma for Smooth Functions). Suppose \(M\) is a smooth manifold with or without boundary, \(A \subseteq M\) is a closed subset, and \(f \colon A \to \mathbb{R}^{k}\) is a smooth function. For any open subset \(U\) containing \(A\) there exists a smooth function \(\widetilde{f} \colon M \to \mathbb{R}^{k}\) with \(\widetilde{f}|_{A} = f\) and \(\operatorname{supp}\widetilde{f} \subseteq U\).
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has Tietze extension, smooth approximation with equality on a closed set when an ambient map is already smooth near that set, and partition-of-unity gluing. No single checked theorem takes Lee’s locally extendable map A → ℝ^k and returns a global smooth extension with topological support inside an arbitrary prescribed open U; proving that would reconstruct the substantive extension lemma rather than map an existing owner. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Proposition 2.28
Proposition 2.28 (Existence of Smooth Exhaustion Functions). Every smooth manifold with or without boundary admits a smooth positive exhaustion function.
Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has compact exhaustions, partitions of unity, and smooth approximation, but no checked theorem constructs a positive smooth proper/exhaustion function on every smooth manifold. No complete external Lean owner was found in the indexed/local reference search. Strict bundle semantics reject proper subsets, terminology-only analogies, specializations, and unbridged ingredients.
Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca
Theorem 2.29
Example 1.32. Theorem 2.29 (Level Sets of Smooth Functions). Let M be a smooth manifold. If K is any closed subset of M; there is a smooth nonnegative function f \(M \to \mathbb { R }\)
Formalized. Mathlib/Geometry/Manifold/PartitionOfUnity.lean::exists_contMDiff_zero_iff_one_iff_of_isClosed — Specializing the theorem to the closed pair (K, ∅) gives a smooth function with values in [0,1] whose zero locus is exactly K; hence it is nonnegative and realizes Lee’s theorem. The specialization compiled at P.