FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013)
FC08 — Lee, Introduction to Smooth Manifolds.
This chapter contains 18 definitions, 4 theorems, 8 propositions, 3 lemmas, 20 examples, 7 conventions and 1 other statements.
Of the 61 statements checked against Lean, 18 are formalized somewhere and 43 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 43 | 70% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 18 | 30% | Mathlib states and proves it. |
| checked in total | 61 |
- Canonical source block: FC08 Lee, Chapter 1,
FC08-C01-U001–FC08-C01-U061, exactly 61 unique contiguous rows retrieved from FC08 — Lee, Introduction to Smooth Manifolds throughagent-memory. - Search order followed the Sweep-II contract: 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 work, indexed searches, Reservoir/package material and broad/local Lean reference mirrors. Noproject-existing, importable package, or admissible external reference-port owner was found for a C01 row. - Every promoted Mathlib declaration/path was checked through the project toolchain at the exact pin
P; cited source files were verified withgit cat-file. The compiled audit witness/tmp/fc08-c01-checks.leanalso checked the structural real-manifold assemblies and synthesized countability of connected components fromSecondCountableTopologyplus local path-connectedness. C01 therefore has 18mathlibrows and 43 datedunmatchedrows. - Positive rows are: U001 (topological-manifold structural interface/Hausdorffness), U010 (product topological manifolds and dimension-sum bridge), U013 (local path connectedness, components, countability, open component manifolds), U014 (local compactness), U015 (local finiteness/refinement/paracompactness), U016 (closures of locally finite families), U019 (smooth maps/diffeomorphisms), U020 (transition maps and smooth compatibility), U021 (smooth atlases), U022 (maximal-atlas presentation of smooth structures), U024 (
C^k/real-analytic/complex-analytic variants), U030 (standard smooth Euclidean space), U036–U037 (open submanifolds), U046 (smooth products), U049 (half-space interior/frontier), U060 (product boundary formula), and U061 (smooth invariance of boundary). - U003 is not promoted: no topological invariance-of-dimension theorem was found. U012/U017/U018 are likewise not inferred from second-countability/paracompactness: the exact precompact-coordinate-ball basis, countable arbitrary-basis refinement, and countable-
π₁statements were not found as checked owners. - U008/U042 are deliberately not routed to
EuclideanSpace.instIsManifoldSphere: Mathlib’s sphere atlas is stereographic, while Lee’s rows specify graph-coordinate atlases, and no checked atlas-equivalence bridge was found. The same strict representation rule leaves the real-projective and Grassmann rows unmatched. - The boundary distinction is material.
ModelWithCorners.isBoundaryPoint_iff_of_mem_atlasproves chart-independence forC¹and higher, so it exactly supports smooth U061. The file explicitly explains that the analogous finite-dimensional topological result requires singular homology and is not proved there; therefore U051–U052 and the topological boundary-manifold assertions of U055 are not promoted from preferred-chart definitions or smooth theorems. - U057 is not equated with Mathlib’s
ContDiffWithinAt: Mathlib uses local Taylor-series/derivative data on a set, whereas Lee defines smoothness on arbitrary subsets by local extension to an ambient open set and additionally records the boundary-derivative/Borel characterization. No checked equivalence of these complete interfaces was found. - Broad external discovery found no admissible complete owner for the missing dimension-invariance, precompact-chart, countable-
π₁, real-projective/Grassmann, full-rank-matrix, regular-level-set, or topological-boundary-invariance rows.facebookresearch/atlas-leanwas not credited: the locally mirrored source is research-only CC BY-NC with a no-training rider and containssorry-backed material, so it is not an admissible portable route under the corpus provenance policy. - Current upstream was refreshed on 2026-09-07:
H=5315eef9e4ffb98e0f89f278b765c50a149f66cawas the Mathlibmasterhead at audit time and uses Lean 4.34.0-rc2. Current-tree searches for the named missing theorem families did not add a complete owner beyond the pinned interfaces above. N=2026-09-07denotes a dated unmatched result after the prescribed search layers. Strict whole-row semantics apply uniformly: a row is not promoted from a proper subset of its clauses or from a nearby representation lacking the required bridge.
Definition/convention — source terminology/construction
Suppose M is a topological space. We say that M is a topological manifold of dimension n or a topological n-manifold if it has the following properties: M is a Hausdorff space: for every pair of distinct points \(p , q \in M\) ; there are disjoint open subsets \(U , V \subseteq M\) such that \(p \in U\) and \(q \in V .\)
Formalized. Mathlib/Topology/Separation/Hausdorff.lean::T2Space; Mathlib/Geometry/Manifold/ChartedSpace.lean::ChartedSpace, chartAt, atlas; Mathlib/Geometry/Manifold/IsManifold/Basic.lean::IsManifold, modelWithCornersSelf — T2Space is exactly Lee’s Hausdorff condition. A ChartedSpace (EuclideanSpace ℝ (Fin n)) M supplies local homeomorphisms to open Euclidean subsets, while IsManifold (𝓡 n) 0 M is the corresponding topological-manifold structure. The audit witness confirms this structural assembly at the pin.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Convention/notation — source terminology/construction
If M is a topological manifold, we often abbreviate the dimension of M as dim M . Informally, one sometimes writes “Let \(M ^ { n }\) be a manifold” as shorthand for “Let M be a manifold of dimension \(\boldsymbol { n } _ { \cdot } ^ { \prime \prime }\) The superscript n is not part of the name of the manifold, and is usually not included in the notation after the first occ the notation after the first occurrence.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If M is a topological manifold, we often abbreviate the dimension of M as dim M . Informally, one sometimes writes “Let M ^n be a manifold” as shorthand for “Let M be a manifold of dimension n _· ^prime prime The superscript n is not part of the name of the manifold, and is usually not included in the notation after the first occurrence. The source is a prose dimension-notation convention; no distinct Lean declaration is needed or owned by an interface. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Theorem 1.2
Theorem 1.2 (Topological Invariance of Dimension). A nonempty n-dimensional topological manifold cannot be homeomorphic to an m-dimensional manifold unless \(m = n\)
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Topological Invariance of Dimension). A nonempty n-dimensional topological manifold cannot be homeomorphic to an m-dimensional manifold unless m = n No pinned/current/external Lean theorem proving topological invariance of finite manifold dimension was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Definition/convention — source terminology/construction
Let M be a topological n-manifold. A coordinate chart (or just a chart) on M is a pair \(( U , \varphi )\) , where U is an open subset of M and \(\varphi \colon U \to { \widehat { U } }\) is a homeomorphism from U to an open subset \({ \hat { U } } = \varphi ( U ) \subseteq \mathbb { R } ^ { n }\) (Fig. 1.2). By definition of a topological manifold, each point \(p \in M\) is contained in the domain of some chart \(( U , \varphi )\) If \(\varphi ( p ) = 0\) , we say that the chart is centered at p. If \(( U , \varphi )\) is any chart whose domain contains p, it is easy to obtain a new chart centered at p by subtracting the constant vector hart centered at p by subtracting the constant vector \(\varphi ( p )\) .
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let M be a topological n-manifold. A coordinate chart (or just a chart) on M is a pair ( U , φ ) , where U is an open subset of M and φ : U → hat(U) is a homeomorphism from U to an open subset hat(U) = φ ( U ) ⊆ ℝ ^n (Fig. 1.2). By definition of a topological manifold, each point p ∈ M is contained in the domain of some chart ( U , φ ) If φ ( p ) = 0 , we say that the chart is centered at p. If ( U , φ ) is any chart whose domain contains p, it is easy to obtain a new chart centered at p by subtracting the constant vector φ ( p ) . ChartedSpace, chartAt, and OpenPartialHomeomorph formalize charts, but the row also includes Lee’s centered-chart/coordinate-ball-or-cube terminology and constructions, for which no checked whole-row interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Definition/convention — coordinate ball
Given a chart \(( U , \varphi )\) , we call the set U a coordinate domain, or a coordinate neighborhood of each of its points. If, in addition, \(\varphi ( U )\) is an open ball in \(\mathbb { R } ^ { n }\) , then U is called a coordinate ball; if \(\varphi ( U )\) is an open cube, U is a coordinate cube. The map ’ is called a (local) coordinate map, and the component functions \(( x ^ { 1 } , \ldots , x ^ { n } )\) of \(\varphi ,\) defined by \(\varphi ( p ) = \left( x ^ { 1 } ( p ) , \ldots , x ^ { n } ( p ) \right)\) , are called local coordinates on U . We sometimes write things such as \(\ " ( U , \varphi )\) is a chart containing \(p ^ { \prime \prime }\) as shorthand for \(\ " ( U , \varphi )\) is a chart whose domain \(U\) contains \(p . \ '\) If we wish to emphasize the coordinate functions \(\left( x ^ { 1 } , \ldots , x ^ { n } \right)\) instead of the coordinate map \(\varphi _ { \cdot }\) we sometimes denote the chart by \(\left( U , \left( x ^ { 1 } , \ldots , x ^ { n } \right) \right)\) or \(\left( U , \left( x ^ { i } \right) \right)\) ## Examples of Topological Manifolds Here are some simple examples. Example 1.3 (Graphs of Continuous Functions). Let \(U \subseteq \mathbb { R } ^ { n }\) be an open subset, and let \(f \colon U \to { \bar { \mathbb { R } } } ^ { k }\) be a continuous function.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Given a chart ( U , φ ) , we call the set U a coordinate domain, or a coordinate neighborhood of each of its points. If, in addition, φ ( U ) is an open ball in ℝ ^n , then U is called a coordinate ball; if φ ( U ) is an open cube, U is a coordinate cube. The map ’ is called a (local) coordinate map, and the component functions ( x ^1 , … , x ^n ) of φ , defined by φ ( p ) = ( x ^1 ( p ) , … , x ^n ( p ) ) , are called local coordinates on U . We sometimes write things such as ” ( U , φ ) is a chart containing p ^prime prime as shorthand for ” ( U , φ ) is a chart whose domain U contains p . ’ If we wish to emphasize the coordinate functions ( x ^1 , … , x ^n ) instead of the coordinate map φ _· we sometimes denote the chart by ( U , ( x ^1 , … , x ^n ) ) or ( U , ( x ^i ) ) ChartedSpace, chartAt, and OpenPartialHomeomorph formalize charts, but the row also includes Lee’s centered-chart/coordinate-ball-or-cube terminology and constructions, for which no checked whole-row interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.3
(Graphs of Continuous Functions). Let \(U \subseteq \mathbb{R}^{n}\) be an open subset and \(f \colon U \to \mathbb{R}^{k}\) a continuous function. Then the graph \(\Gamma(f)\) is a topological manifold of dimension \(n\); it is homeomorphic to \(U\) itself, and \((\Gamma(f), \varphi)\) is a global coordinate chart, called graph coordinates. The same applies to any subset of \(\mathbb{R}^{n+k}\) defined by setting any \(k\) of the coordinates, not necessarily the last \(k\), equal to a continuous function of the other \(n\), which are restricted to lie in an open subset of \(\mathbb{R}^{n}\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Graphs of Continuous Functions). Let U ⊆ ℝ ^n be an open subset, and let f : U → bar ℝ ^k be a continuous function. Thus Gamma ( f ) is a topological manifold of dimension n. In fact, Gamma ( f ) is homeomorphic to U itself, and ( Gamma ( f ) , φ ) is a global coordinate chart, called graph coordinates. The same observation applies to any subset of ℝ ^n + k defined by setting any k of the coordinates (not necessarily the last k) equal to some continuous function of the other n , which are restricted to lie in an open subset of ℝ ^n Mathlib has graph/homeomorphism infrastructure, but no checked construction giving Lee’s graph manifold together with the stated graph-coordinate chart terminology. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Convention/notation — graph coordinates
\[ Because $\varphi$ is the restriction of a continuous map, it is continuous; and it is a homeomorphism because it has a continuous inverse given by $\varphi ^ { - 1 } ( x ) = ( x , f ( x ) )$ . Thus $\Gamma ( f )$ is a topological manifold of dimension n. In fact, $\Gamma ( f )$ is homeomorphic to U itself, and $( \Gamma ( f ) , \varphi )$ is a global coordinate chart, called graph coordinates. The same observation applies to any subset of $\mathbb { R } ^ { n + k }$ defined by setting any $k$ of the coordinates (not necessarily the last k) equal to some continuous function of the other $n ,$ which are restricted to lie in an open subset of $\mathbb { R } ^ { n }$ Example 1.4 (Spheres). For each integer $n \geq 0$ the unit n-sphere $\mathbb { S } ^ { n }$ is Hausdorff and second-countable because it is a topological subspace of $\mathbb { R } ^ { n + 1 }$ . To show that it is locally Euclidean, for each index $i = 1 , \ldots , n + 1$ let $U _ { i } ^ { + }$ denote the subset of $\mathbb { R } ^ { n + 1 }$ where the i th coordinate is positive: \]
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Because φ is the restriction of a continuous map, it is continuous; and it is a homeomorphism because it has a continuous inverse given by φ ^- 1 ( x ) = ( x , f ( x ) ) . Thus Gamma ( f ) is a topological manifold of dimension n. In fact, Gamma ( f ) is homeomorphic to U itself, and ( Gamma ( f ) , φ ) is a global coordinate chart, called graph coordinates. The same observation applies to any subset of ℝ ^n + k defined by setting any k of the coordinates (not necessarily the last k) equal to some continuous function of the other n , which are restricted to lie in an open subset of ℝ ^n // Mathlib has graph/homeomorphism infrastructure, but no checked construction giving Lee’s graph manifold together with the stated graph-coordinate chart terminology. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.4
(Spheres). For each integer \(n \geq 0\) the unit \(n\)-sphere \(\mathbb{S}^{n}\) is Hausdorff and second-countable, being a topological subspace of \(\mathbb{R}^{n+1}\). Each subset \(U_{i}^{\pm} \cap \mathbb{S}^{n}\) is locally Euclidean of dimension \(n\), and the maps \(\varphi_{i}^{\pm} \colon U_{i}^{\pm} \cap \mathbb{S}^{n} \to \mathbb{B}^{n}\) given by \(\varphi_{i}^{\pm}(x^{1},\dots,x^{n+1}) = (x^{1},\dots,\widehat{x}^{i},\dots,x^{n+1})\) are graph coordinates for \(\mathbb{S}^{n}\). Since every point of \(\mathbb{S}^{n}\) lies in the domain of at least one of these \(2n+2\) charts, \(\mathbb{S}^{n}\) is a topological \(n\)-manifold.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Spheres). For each integer n ≥ 0 the unit n-sphere mathbb S ^n is Hausdorff and second-countable because it is a topological subspace of ℝ ^n + 1 . Thus, each subset U i ^± ∩ mathbb S ^n is locally Euclidean of dimension n : , and the maps φ _i ^± : U _i ^± ∩ mathbb S ^n → mathbb B ^n given by varphi_i ^± big (x ^1, … , x ^n + 1 big) = big (x ^1, … , widehat x ^i, … , x ^n + 1 big) are graph coordinates for mathbb S ^n . Since each point of mathbb S ^n is in the domain of at least one of these 2 n + 2 charts, mathbb S ^n is a topological n-manifold. EuclideanSpace.instIsManifoldSphere gives the sphere an analytic manifold structure via stereographic charts; no checked bridge identifies this with Lee’s specific graph-chart construction in the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.5
Example 1.5 (Projective Spaces). The n-dimensional real projective space, denoted by \(\mathbb { R P } ^ { n }\) (or sometimes just \(\mathbb { P } ^ { n } )\) , is defined as the set of 1-dimensional linear subspaces of \(\mathbb { R } ^ { n + 1 }\) , with the quotient topology determined by the natural map \(\pi \colon \mathbb { R } ^ { n + 1 } \setminus \{ 0 \} \to \mathbb { R P } ^ { n }\) sending each point \(x \in \mathbb { R } ^ { n + 1 } \setminus \{ 0 \}\) to the subspace spanned by x. The 2-dimensional projective space \(\mathbb { R P } ^ { 2 }\) is called the projective plane. For any point \(x \in \mathbb { R } ^ { n + 1 } \setminus \{ 0 \}\) , let \([ x ] = \pi ( x ) \in \mathbb { R P } ^ { n }\) denote the line spanned by x. For each \(i = 1 , \ldots , n + 1\) let \(\widetilde { U } _ { i } \subseteq \mathbb { R } ^ { n + 1 } \setminus \{ 0 \}\) be the set where \(x ^ { i } \neq 0\) and let \(U _ { i } = \pi ( \widetilde { U } _ { i } ) \subseteq \mathbb { R P } ^ { n }\) Since \(\widetilde { U } _ { i }\) is a saturated open subset, \(U _ { i }\) is open and \(\pi | _ { \widetilde { U } _ { i } } \colon \widetilde { U } _ { i } \to U _ { i }\)
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Projective Spaces). The n-dimensional real projective space, denoted by mathbb R P ^n (or sometimes just mathbb P ^n ) , is defined as the set of 1-dimensional linear subspaces of ℝ ^n + 1 , with the quotient topology determined by the natural map π : ℝ ^n + 1 setminus 0 → mathbb R P ^n sending each point x ∈ ℝ ^n + 1 setminus 0 to the subspace spanned by x. The 2-dimensional projective space mathbb R P ^2 is called the projective plane. For any point x ∈ ℝ ^n + 1 setminus 0 , let [ x ] = π ( x ) ∈ mathbb R P ^n denote the line spanned by x. No checked finite-dimensional real projective-space manifold construction with Lee’s quotient charts was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.8
(Product Manifolds). Suppose \(M_{1},\dots,M_{k}\) are topological manifolds of dimensions \(n_{1},\dots,n_{k}\). The product map \(\varphi_{1} \times \cdots \times \varphi_{k} \colon U_{1} \times \cdots \times U_{k} \to \mathbb{R}^{n_{1}+\cdots+n_{k}}\) is a homeomorphism onto its image, a product open subset of \(\mathbb{R}^{n_{1}+\cdots+n_{k}}\). Thus \(M_{1} \times \cdots \times M_{k}\) is a topological manifold of dimension \(n_{1}+\cdots+n_{k}\), with charts \((U_{1} \times \cdots \times U_{k},\ \varphi_{1} \times \cdots \times \varphi_{k})\): given any point \((p_{1},\dots,p_{k})\), choose a chart \((U_{i},\varphi_{i})\) for each \(M_{i}\) with \(p_{i} \in U_{i}\).
Formalized. Mathlib/Geometry/Manifold/ChartedSpace.lean::prodChartedSpace, prodChartedSpace_chartAt; Mathlib/Geometry/Manifold/IsManifold/Basic.lean::IsManifold.prod; Mathlib/Analysis/InnerProductSpace/PiL2.lean::EuclideanSpace.finAddEquivProd — prodChartedSpace forms product charts and prodChartedSpace_chartAt identifies the preferred chart componentwise; IsManifold.prod proves the product is again a topological manifold. EuclideanSpace.finAddEquivProd is the explicit linear homeomorphism ℝ^(n+m) ≃ ℝ^n × ℝ^m, providing the dimension-sum bridge. Finite products follow by iteration.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Example 1.9
Example 1.9 (Tori). For a positive integer n, the n-torus (plural: tori) is the product space \(\mathbb { T } ^ { n } = \mathbb { S } ^ { 1 } \times \cdots \times \mathbb { S } ^ { 1 }\) . By the discussion above, it is a topological n-manifold. (The 2-torus is usually called simply mage, which is a product open subset of \(\mathbb { R } ^ { n _ { 1 } + \cdots + n _ { k } }\) Thus, \(M _ { 1 } \times \cdots \times M _ { k }\) is a topological manifold of dimension \(n _ { 1 } + \cdots + n _ { k }\) , with charts of the form \(( U _ { 1 } \times \cdots \times U _ { k } , \varphi _ { 1 } \times \cdots \times \varphi _ { k } )\) // Example 1.9 (Tori).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Tori). For a positive integer n, the n-torus (plural: tori) is the product space mathbb T ^n = mathbb S ^1 × ·s × mathbb S ^1 . By the discussion above, it is a topological n-manifold. (The 2-torus is usually called simply the torus.) // Sphere and binary product manifold instances exist, but no checked arbitrary-n torus-as-finite-product manifold package realizes the whole example. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Lemma 1.10
Lemma 1.10. Every topological manifold has a countable basis of precompact coordinate balls.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every topological manifold has a countable basis of precompact coordinate balls. Second-countability and local compactness machinery exists, but no checked theorem supplies Lee’s countable basis of precompact coordinate balls. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Proposition 1.11
Proposition 1.11. Let M be a topological manifold. (a) M is locally path-connected. (b) M is connected if and only if it is path-connected. (c) The components of M are the same as its path components. (d) M has countably many components, each of which is an open subset of M and a connected topological manifold.
Formalized. Mathlib/Geometry/Manifold/ChartedSpace.lean::ChartedSpace.locallyPathConnectedSpace; Mathlib/Topology/Connected/LocallyPathConnected.lean::pathConnectedSpace_iff_connectedSpace, pathComponent_eq_connectedComponent; Mathlib/Topology/Connected/LocallyConnected.lean::isOpen_connectedComponent; Mathlib/Topology/Connected/Basic.lean::isConnected_connectedComponent; Mathlib/Geometry/Manifold/HasGroupoid.lean::TopologicalSpace.Opens.instChartedSpace; Mathlib/Geometry/Manifold/IsManifold/Basic.lean::TopologicalSpace.Opens.instIsManifold — Finite-dimensional Euclidean models are locally path-connected, so ChartedSpace.locallyPathConnectedSpace gives (a). In such spaces connectedness equals path-connectedness and connected components equal path components; connected components are open. The project-pin audit also synthesized Countable (ConnectedComponents M) from SecondCountableTopology M plus local path-connectedness. Treating each open component as an Opens M inherits its charted/manifold structure, while isConnected_connectedComponent gives connectedness. This realizes all clauses (a)–(d).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 1.12
Proposition 1.12 (Manifolds Are Locally Compact). Every topological manifold is locally compact.
Formalized. Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean::Manifold.locallyCompact_of_finiteDimensional — Manifold.locallyCompact_of_finiteDimensional states exactly that a manifold modelled on a finite-dimensional space over a locally compact field is locally compact. Specializing to ℝ and EuclideanSpace ℝ (Fin n) gives Lee’s proposition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — refinement of U
Let M be a topological space. A collection of subsets of M is said to be locally finite if each point of M has a neighborhood that intersects at most finitely many of the sets in . Given a cover of M; another cover is called a refinement of if for each \(V \in \mathcal V\) there exists some \(U \in \mathcal { U }\) such that \(V \subseteq U\) . We say that M is paracompact if every open cover of M admits an open, locally finite is a consequence of local compactness and second-countability, and in fact is one of the main reasons why second-countability is included in the definition of manifolds.
Formalized. Mathlib/Topology/LocallyFinite.lean::LocallyFinite; Mathlib/Topology/Compactness/Paracompact.lean::ParacompactSpace, precise_refinement — LocallyFinite uses exactly a neighborhood meeting only finitely many members. ParacompactSpace says every indexed open cover has an open locally finite refinement, and precise_refinement provides the refinement/subordination relation explicitly. This is Lee’s complete terminology bundle.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Lemma 1.13
Suppose \(\mathcal{X}\) is a locally finite collection of subsets of a topological space \(M\). (a) The collection \(\{\overline{X} : X \in \mathcal{X}\}\) is also locally finite. (b) \(\overline{\bigcup_{X \in \mathcal{X}} X} = \bigcup_{X \in \mathcal{X}} \overline{X}\).
Formalized. Mathlib/Topology/LocallyFinite.lean::LocallyFinite.closure, LocallyFinite.closure_iUnion — LocallyFinite.closure proves that closures of a locally finite family remain locally finite, and LocallyFinite.closure_iUnion proves closure (⋃ i, f i) = ⋃ i, closure (f i), exactly the two assertions in the row.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 1.15
Theorem 1.15 (Manifolds Are Paracompact). Every topological manifold is paracompact. In fact, given a topological manifold M; an open cover of M; and any basis for the topology of M; there exists a countable, locally finite open refinement of consisting of elements ment.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Manifolds Are Paracompact). Every topological manifold is paracompact. In fact, given a topological manifold M; an open cover X of M; and any basis B for the topology of M; there exists a countable, locally finite open refinement of X consisting of elements of B . ParacompactSpace and precise locally finite refinements are pinned, but Lee’s strengthened clause requires a countable refinement consisting of elements of an arbitrary prescribed basis; no checked theorem supplies that full strengthening. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Proposition 1.16
Proposition 1.16. The fundamental group of a topological manifold is countable.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The fundamental group of a topological manifold is countable. No checked theorem showing the fundamental group of every topological manifold is countable was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Definition/convention — diffeomorphism
The definition will be based on the calculus of maps between Euclidean spaces, so let us begin by reviewing some basic terminology about such maps. If U and V are open subsets of Euclidean spaces \(\mathbb { R } ^ { n }\) and \(\mathbb { R } ^ { m }\) , respectively, a function \(F \colon U \to V\) is said to be smooth (or \(C ^ { \infty }\) , or infinitely differentiable) if each of its component functions has continuous partial derivatives of all orders. If in addition F is bijective and has a smooth inverse map, it is called a diffeomorphism. A diffeomorphism is, in particular, a homeomorphism. A review of some important properties of smooth maps is given in Appendix C. You should be aware that some authors define the word smooth differently—for example, to mean continuously differentiable or merely differentiable. On the other hand, some use the word differentiable to mean what we call smooth. Throughout this book, smooth is synonymo manifold are smooth.
Formalized. Mathlib/Analysis/Calculus/ContDiff/Defs.lean::ContDiff; Mathlib/Geometry/Manifold/Diffeomorph.lean::Diffeomorph, Diffeomorph.continuous — ContDiff ℝ ∞ is Mathlib’s Fréchet-calculus presentation of smoothness, equivalent on finite-dimensional Euclidean spaces to continuous partial derivatives of all orders. Diffeomorph is an equivalence whose forward and inverse maps are ContMDiff; Diffeomorph.continuous records the resulting homeomorphism property. This is the same smooth/diffeomorphism notion in an invariant formalization.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — transition map
Let M be a topological n-manifold. If \(( U , \varphi ) , ( V , \psi )\) are two charts such that \(U \cap V \neq \emptyset\) , the composite map \(\circ \varphi ^ { - 1 } \colon \varphi ( U \cap V ) \to \psi ( U \cap V )\) is called the transition map from ’ to (Fig. 1.6). It is a composition of homeomorphisms, and is therefore itself a homeomorphism. Two charts \(( U , \varphi )\) and \(( V , \psi )\) are said to be smoothly compatible if either \(U \cap V = \emptyset\) or the transition map \(\psi \circ \varphi ^ { - 1 }\) is a diffeomorphism. Since \(\varphi ( U \cap V )\) and \(\psi ( U \cap V )\) are open subsets of \(\mathbb { R } ^ { n }\) , smoothness of this map is to be interpreted in the ordinary sense of having continuous partial derivatives of al th charts.” Since smoothness is not a homeomorphism-invariant property, the way to do this is to consider the collection of all smooth charts as a new kind of structure on M .
Formalized. Mathlib/Geometry/Manifold/HasGroupoid.lean::HasGroupoid.compatible, StructureGroupoid.compatible; Mathlib/Geometry/Manifold/IsManifold/Basic.lean::contDiffGroupoid; Mathlib/Topology/OpenPartialHomeomorph/Composition.lean::OpenPartialHomeomorph.trans — For charts e,e′, Mathlib’s coordinate change is e.symm ≫ₕ e′; the HasGroupoid.compatible field requires this transition to belong to the chosen structure groupoid. With contDiffGroupoid ∞ I, membership is precisely smooth compatibility (the empty-overlap case is included by restriction/locality).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — smooth atlas
We define an atlas for M to be a collection of charts whose domains cover M . An atlas is called a smooth atlas if any two charts in are smoothly compatible with each other. T
Formalized. Mathlib/Geometry/Manifold/ChartedSpace.lean::ChartedSpace, atlas, iUnion_source_chartAt; Mathlib/Geometry/Manifold/HasGroupoid.lean::HasGroupoid, HasGroupoid.compatible — ChartedSpace stores an atlas of charts together with preferred charts whose sources cover the space (iUnion_source_chartAt). HasGroupoid adds pairwise compatibility of atlas charts; for the smooth groupoid this is exactly a smooth atlas.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — differentiable structures
complete.) Now we can define the main concept of this chapter. If M is a topological manifold, a smooth structure on M is a maximal smooth atlas. A smooth manifold is a pair \(( M , { \mathcal { A } } )\) , where M is a topological manifold and is a smooth structure on M . When the smooth structure is understood, we usually omit mention of it and just say \(^ { 6 6 } M\) is a smooth manifold.” Smooth structures are also called differentiable structures or \(C ^ { \infty }\) structures by some authors. We also use the term smooth manifold structure to mean a manifold topology together with a smooth struc f it is smooth in the sense of ordinary calculus.
Formalized. Mathlib/Geometry/Manifold/IsManifold/Basic.lean::IsManifold, IsManifold.maximalAtlas, IsManifold.subset_maximalAtlas; Mathlib/Geometry/Manifold/HasGroupoid.lean::StructureGroupoid.maximalAtlas, StructureGroupoid.compatible_of_mem_maximalAtlas — Mathlib presents a smooth manifold by a charted space with a smooth structure groupoid, then canonically forms maximalAtlas of all charts compatible with that structure. subset_maximalAtlas embeds the chosen atlas and compatible_of_mem_maximalAtlas makes the maximal atlas pairwise compatible. This is the standard equivalent presentation of Lee’s “smooth structure = maximal smooth atlas.”
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 1.17
Proposition 1.17. Let M be a topological manifold. (a) Every smooth atlas for M is contained in a unique maximal smooth atlas, called the smooth structure determined by (b) Two smooth atlases for M determine the same smooth structure if and only if their union is a smooth atlas.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let M be a topological manifold. (a) Every smooth atlas A for M is contained in a unique maximal smooth atlas, called the smooth structure determined by A . (b) Two smooth atlases for M determine the same smooth structure if and only if their union is a smooth atlas. maximalAtlas is defined and contains the chosen atlas, but no checked theorem realizes both Lee clauses: uniqueness for an arbitrary smooth atlas and equality of induced structures iff the union atlas is smooth. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Comparison/convention — a C
It is worth mentioning that the notion of smooth structure can be generalized in several different ways by changing the compatibility requirement for charts. For example, if we replace the requirement that charts be smoothly compatible by the weaker requirement that each transition map \(\circ \varphi ^ { - 1 }\) (and its inverse) be of class \(C ^ { k }\) , we obtain the definition of a \(C ^ { k }\) structure. Similarly, if we require that each transition map be real-analytic (i.e., expressible as a convergent power series in a neighborhood of each point), we obtain the definition of a real-analytic structure, also called \(\operatorname { a } { \mathbf { } C } ^ { \omega }\) structure. If M has even dimension \(n = 2 m\) , we can identify \(\mathbb { R } ^ { 2 m }\) with \(\mathbb { C } ^ { m }\) and require that the transition maps be complex-analytic; this determines a complex-analytic structure. A manifold endowed with one of these structures is called a \(C ^ { k }\) manifold, real-analytic manifold, or complex manifold, respectively. (Note that a \(C ^ { 0 }\) manifold is just a topological manifold.) We do not treat any of these other kinds of manifolds in this book, but they play important roles in analysis, so it is useful single chart, the smooth compatibility condition is trivially satisfied, so any such chart automatically determines a smooth structure on \(M\) It is worth mentioning that the notion of smooth structure can be generalized in several different ways by changing the compatibility requirement for charts.
Formalized. Mathlib/Geometry/Manifold/IsManifold/Basic.lean::IsManifold, contDiffGroupoid, IsManifold.of_le — IsManifold I n M is parameterized by n : ℕ∞ω: finite n gives C^k, ∞ smooth, ω analytic, and n=0 topological. The scalar field/model parameter also permits ℝ versus ℂ, so the same interface covers Lee’s real-analytic and complex-analytic variants.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — smooth chart
Local Coordinate Representations If M is a smooth manifold, any chart \(( U , \varphi )\) contained in the given maximal smooth atlas is called a smooth chart, and the corresponding coordinate map \(\varphi\) is called a smooth coordinate map. It is useful also to introduce the terms smooth coordinate domain or smooth coordinate neighborhood for the domain of a smooth coordinate chart. A smooth coordinate ball means a smooth coordinate domain whose image under a smooth coordinate map is a ball in Euclidean space. A smooth coordinate regular coordinate ball if } { B }$ and a smooth coordinate map ’ $
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If M is a smooth manifold, any chart ( U , φ ) contained in the given maximal smooth atlas is called a smooth chart, and the corresponding coordinate map φ is called a smooth coordinate map. It is useful also to introduce the terms smooth coordinate domain or smooth coordinate neighborhood for the domain of a smooth coordinate chart. A smooth coordinate ball means a smooth coordinate domain whose image under a smooth coordinate map is a ball in Euclidean space. A smooth coordinate cube is defined similarly Maximal smooth atlases and charts are formalized, but Lee’s smooth/regular coordinate-ball terminology and the countable regular-coordinate-ball basis are not owned by a checked declaration. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Definition/convention — regular coordinate ball
A set \(B \subseteq M\) is a regular coordinate ball if there is a smooth coordinate ball \(B' \supseteq \overline{B}\) and a smooth coordinate map \(\varphi \colon B' \to \mathbb{R}^{n}\) such that, for some \(0 < r < r'\), \[ \varphi(B) = B_{r}(0), \qquad \varphi(\overline{B}) = \overline{B}_{r}(0), \qquad\text{and}\qquad \varphi(B') = B_{r'}(0). \] In particular \(\overline{B}\) is compact, being homeomorphic to a closed Euclidean ball.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: It is often useful to restrict attention to coordinate balls whose closures sit nicely inside larger coordinate balls. We say a set B ⊆ M is a regular coordinate ball if there is a smooth coordinate ball B ^prime supseteq bar(B) and a smooth coordinate map ’ B ^prime → ℝ ^n such that for some positive real numbers beginarray r r < r ^prime , endarray Maximal smooth atlases and charts are formalized, but Lee’s smooth/regular coordinate-ball terminology and the countable regular-coordinate-ball basis are not owned by a checked declaration. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Proposition 1.19
Proposition 1.19. Every smooth manifold has a countable basis of regular coordinate balls. E
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every smooth manifold has a countable basis of regular coordinate balls. Maximal smooth atlases and charts are formalized, but Lee’s smooth/regular coordinate-ball terminology and the countable regular-coordinate-ball basis are not owned by a checked declaration. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Convention/notation — source terminology/construction
Another way to look at it is that by means of our identification \(U \hat { U }\) , we can think of \(\varphi\) as the identity map and suppress it from the notation. This takes a bit of getting used to, but the payoff is a huge simplification of the notation in many situations. You just need to remember that the identification is in general only local, and depends heavily on the choice of coordinate chart.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Another way to look at it is that by means of our identification U hat(U) , we can think of φ as the identity map and suppress it from the notation. This takes a bit of getting used to, but the payoff is a huge simplification of the notation in many situations. You just need to remember that the identification is in general only local, and depends heavily on the choice of coordinate chart. This is a notation/suppression convention rather than a mathematical interface with a distinct Lean owner. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.21
Example 1.21 (0-Dimensional Manifolds). A topological manifold M of dimension 0 is just a countable discrete space. For each point \(p \in M .\) ; the only neighborhood of \(p\) that is homeomorphic to an open subset of \(\mathbb { R } ^ { 0 }\) is \(\{ p \}\) itself, and there is exactly one coordinate map \(\varphi \colon \{ p \} \mathbb { R } ^ { 0 }\) Thus, the set of all charts on M trivially satisfies the smooth compatibility condition, and each 0-dimensional manifold has a unique sm objects we wish to define globally on a manifold are not dependent on a particular choice of coordinates.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (0-Dimensional Manifolds). A topological manifold M of dimension 0 is just a countable discrete space. For each point p ∈ M . ; the only neighborhood of p that is homeomorphic to an open subset of ℝ ^0 is p itself, and there is exactly one coordinate map φ : p ℝ ^0 Thus, the set of all charts on M trivially satisfies the smooth compatibility condition, and each 0-dimensional manifold has a unique smooth structure. Discrete charted-space constructors exist, but no checked whole-row theorem identifies 0-manifolds with countable discrete spaces and proves uniqueness of the smooth structure. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.22
Example 1.22 (Euclidean Spaces). For each nonnegative integer n, the Euclidean space \(\mathbb { R } ^ { n }\) is a smooth n-manifold with the smooth structure determined by the atlas consisting of the single chart \(( \mathbb { R } ^ { n } , \operatorname { I d } _ { \mathbb { R } ^ { n } } )\) . We call this the standard smooth structure on \(\mathbb { R } ^ { n }\) and the resulting coordinate map standard coordinates. Unless we explicitly specify otherwise, we always use this smooth structure on \(\mathbb { R } ^ { n }\) . With respect to this smooth structure, the smooth coordinate charts for \(\mathbb { R } ^ { n }\) are exactly those charts \(( U , \varphi )\) such that \(\varphi\) is a diffeomorphism (in the sense of ordinary calculus)
Formalized. Mathlib/Geometry/Manifold/ChartedSpace.lean::chartedSpaceSelf, chartedSpaceSelf_atlas; Mathlib/Geometry/Manifold/IsManifold/Basic.lean::IsManifold.instIsManifoldModelSpace, modelWithCornersSelf — chartedSpaceSelf uses the identity chart on a model space, and instIsManifoldModelSpace makes every model space a C^n manifold for all regularities. Specialization to the real Euclidean model 𝓡 n is exactly the standard smooth structure on ℝ^n.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Example 1.23
another open subset \({ \hat { U } } \subseteq \mathbb { R } ^ { n }\) Example 1.23 (Another Smooth Structure on ). Consider the homeomorphism $: $ R given by \[ \psi (x) = x ^ {3}.\tag{1.1} \] The atlas consisting of the single chart \(( \mathbb { R } , \psi )\) defines a smooth structure on R. This chart is not smoothly compatible with the standard smooth structure, because the transition map IdR \(\circ \psi ^ { - 1 } ( y ) = y ^ { 1 / 3 }\) is not smooth at the origin. Therefore, the smooth structure defined on R by is not the same as the standard one. Using similar ideas, it is not hard to construct many distinct smooth structures on any given positive-dimensional topological manifold, as long as it has one smooth structure to begin with (see fold has a unique smooth structure.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Another Smooth Structure on R ). Consider the homeomorphism ψ : ℝ → R given by ψ (x) = x ^3.tag1.1 The atlas consisting of the single chart ( ℝ , ψ ) defines a smooth structure on R. This chart is not smoothly compatible with the standard smooth structure, because the transition map IdR ∘ ψ ^- 1 ( y ) = y ^1 / 3 is not smooth at the origin. Therefore, the smooth structure defined on R by is not the same as the standard one. Using similar ideas, it is not hard to construct many distinct smooth structures on any given positive-dimensional topological manifold, as long as it has one smooth structure to begin with (see Problem 1-6). No checked construction of Lee’s x ↦ x^3 exotic atlas on ℝ together with its incompatibility with the standard structure was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.24
(Finite-Dimensional Vector Spaces). Let \(V\) be a finite-dimensional real vector space. For two bases the coordinates are related by \(\widetilde{x}^{j} = \sum_{i} A^{j}_{i} x^{i}\), so the map sending \(x\) to \(\widetilde{x}\) is an invertible linear map and hence a diffeomorphism; any two such charts are smoothly compatible. The collection of all such charts defines a smooth structure, the standard smooth structure on \(V\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Finite-Dimensional Vector Spaces). Let V be a finite-dimensional real vector space. It follows that tilde(x) ^j = sum _i A _i ^j x ^i Thus, the map sending x to tilde(x) is an invertible linear map and hence a diffeomorphism, so any two such charts are smoothly compatible. The collection of all such charts thus defines a smooth structure, called the standard smooth structure on V . Normed vector spaces are model manifolds in Mathlib, but the row asserts the canonical basis-independent smooth structure on an arbitrary finite-dimensional real vector space; no checked bridge proving that basis independence was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Convention/notation — Einstein summation convention
We interpret any such expression according to the following rule, called the Einstein summation convention: if the same index name (such as i in the expression above) appears exactly twice in any monomial term, once as an upper index and once as a lower index, that term is understood to be summed over all possible values of that index, generally from 1 to the dimension of the space in question. This simple idea was introduced by Einstein to reduce the complexity of expressions arising in the study of smooth manifolds by eliminating the necessity of explicitly writing summation signs. We use the summation convention systematically throughout the book (except in the appendices, which many readers will look at before the rest of the book).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: We interpret any such expression according to the following rule, called the Einstein summation convention: if the same index name (such as i in the expression above) appears exactly twice in any monomial term, once as an upper index and once as a lower index, that term is understood to be summed over all possible values of that index, generally from 1 to the dimension of the space in question. This simple idea was introduced by Einstein to reduce the complexity of expressions arising in the study of smooth manifolds by eliminating the necessity of explicitly writing summation signs. We use the summation convention systematically throughout the book (except in the appendices, which many readers will look at before the rest of the book). This is an index/summation notation convention rather than a distinct formal theorem or construction. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Convention/notation — expression is unchanged
Another important aspect of the summation convention is the positions of the indices. We always write basis vectors (such as \(E _ { i } )\) with lower indices, and components of a vector with respect to a basis (such as \(\overline { { x ^ { i } ) } }\) with upper indices. These index conventions help to ensure that, in summations that make mathematical sense, each index to be summed over typically appears twice in any given term, once as a lower index and once as an upper index. Any index that is implicitly summed over is a “dummy index,” meaning that the value of such an expression is unchanged if a different name is substituted for each dummy index. For example, \(x ^ { i } E _ { i }\) and \(x ^ { j } E _ { j }\) mean exactly the same nifolds.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Another important aspect of the summation convention is the positions of the indices. We always write basis vectors (such as E _i ) with lower indices, and components of a vector with respect to a basis (such as overline x ^i ) with upper indices. These index conventions help to ensure that, in summations that make mathematical sense, each index to be summed over typically appears twice in any given term, once as a lower index and once as an upper index. Any index that is implicitly summed over is a “dummy index,” meaning that the value of such an expression is unchanged if a different name is substituted for each dummy index. For example, x ^i E _i and x ^j E _j mean exactly the same thing. This is an index/summation notation convention rather than a distinct formal theorem or construction. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.25
mn under matrix addition and scalar multiplication, \(\mathbf { M } ( m \times n , \mathbb { R } )\) is a smooth mn-dimensional manifold. (In fact, it is often useful to identify \(\mathbf { M } ( m \times n , \mathbb { R } )\) with \(\mathbb { R } ^ { m n }\) , just by stringing all the matrix entries out in a single row.) Similarly, the space \(\mathbf { M } ( { \boldsymbol { m } } \times { \boldsymbol { n } } , \mathbb { C } )\) of \(m \times n\) complex matrices is a vector space of dimension 2mn over R, and thus a smooth manifold of dimension 2mn. In the special case in which \(m = n\) (square matrices), we abbreviate \(\mathbf { M } ( n \times n , \mathbb { R } )\) and \(\mathbf { M } ( n \times n , \mathbb { C } )\) by \(\mathbf { M } ( n , \mathbb { R } )\) and \(\mathbf { M } ( n , \mathbb { C } )\) , respectively. Example 1.26 (Open Submanifolds). Let U be any open subset of \(\mathbb { R } ^ { n }\) . Then U is a topological s for these coordinates, and we do so throughout this book.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Spaces of Matrices). Let M ( m × n , ℝ ) denote the set of m × n matrices with real entries. (In fact, it is often useful to identify M ( m × n , ℝ ) with ℝ ^m n , just by stringing all the matrix entries out in a single row.) Similarly, the space M ( m × n , ℂ ) of m × n complex matrices is a vector space of dimension 2mn over R, and thus a smooth manifold of dimension 2mn. In the special case in which m = n (square matrices), we abbreviate M ( n × n , ℝ ) and M ( n × n , ℂ ) by M ( n , ℝ ) and M ( n , ℂ ) , respectively. // Matrix types inherit finite-dimensional linear/topological structure, but no checked whole-row declaration packages all real/complex matrix-space manifold dimensions stated here. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.26
(Open Submanifolds). Let \(U\) be any open subset of \(\mathbb{R}^{n}\). Then \(U\) is a topological \(n\)-manifold, and the single chart \((U, \operatorname{Id}_{U})\) defines a smooth structure on \(U\).
Formalized. Mathlib/Geometry/Manifold/HasGroupoid.lean::Topology.IsOpenEmbedding.singletonChartedSpace; Mathlib/Geometry/Manifold/IsManifold/Basic.lean::Topology.IsOpenEmbedding.isManifold_singleton — For an open subset U ⊆ ℝ^n, the subtype inclusion is an open embedding. singletonChartedSpace builds the charted space from that single inclusion chart, and isManifold_singleton proves it is a C^n manifold for every regularity. Thus the identity/inclusion chart gives exactly Lee’s standard smooth open-submanifold structure.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — open submanifold
Every point \(p \in U\) is contained in the domain of some chart \(( W , \varphi )\) for M ; if we set \(V = W \cap U\) , then \(( V , \varphi | _ { V } )\) is a chart in \(\mathbf { \mathcal { A } } _ { U }\) whose domain contains p. Therefore, U is covered by the domains of charts in \({ \mathcal { A } } _ { U } ,\) and it is easy to verify that this is a smooth atlas for U . Thus any open subset of M is itself a smooth n-manifold in a natural way. Endowed with this smooth structure, we call any open subset an open submanifold of M . (We will define a more general class of submanifolds in Chapter 5.)
Formalized. Mathlib/Geometry/Manifold/HasGroupoid.lean::TopologicalSpace.Opens.instChartedSpace, TopologicalSpace.Opens.instHasGroupoid, TopologicalSpace.Opens.chartAt_eq; Mathlib/Geometry/Manifold/IsManifold/Basic.lean::TopologicalSpace.Opens.instIsManifold — An Opens M inherits charts by restricting ambient charts (chartAt_eq), inherits the structure groupoid, and is an IsManifold I n. This is precisely Lee’s natural smooth structure on every open subset and hence his open-submanifold convention.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Example 1.27
Example 1.27 (The General Linear Group). The general linear group GL.n; R/ is the set of invertible \(n \times n\) matrices with real entries. It is a smooth \(n ^ { 2 } .\) -dimensional manifold because it is an open subset of the \(n ^ { 2 }\) -dimensional vector space \(\mathbf { M } ( n , \mathbb { R } )\) , namely the set where the (continuous) determinant function th \(\mathbb { R } ^ { m n }\) , just by stringing all the matrix entries out in a single row.) Similarly, the space \(\mathbf { M } ( { \boldsymbol { m } } \times { \boldsymbol { n } } , \mathbb { C } )\) of \(m \times n\) complex matrices is a vector space of dimension 2mn over R, and thus a smooth manifold of dimension 2mn.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (The General Linear Group). The general linear group GL.n; R/ is the set of invertible n × n matrices with real entries. It is a smooth n ^2 . -dimensional manifold because it is an open subset of the n ^2 -dimensional vector space M ( n , ℝ ) , namely the set where the (continuous) determinant function is nonzero // Mathlib has Lie-manifold infrastructure for units of normed algebras and continuous-linear-map spaces, but no checked bridge realizes Lee’s exact finite matrix GL(n,ℝ), full-rank rectangular-matrix open locus, or algebraic L(V,W) dimension bundle. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.28
subset of \(\mathbf { M } ( m \times n , \mathbb { R } )\) consisting of matrices of rank m. If A is an arbitrary such matrix, the fact that rank \(A = m\) means that A has some nonsingular \(m \times m\) submatrix. By continuity of the determinant function, this same submatrix has nonzero determinant on a neighborhood of A in \(\mathbf { M } ( m \times n , \mathbb { R } )\) , which implies that A has a neighborhood contained in \(\mathbf { M } _ { m } ( m \times n , \mathbb { R } )\) Thus, \(\mathbf { M } _ { m } ( m \times n , \mathbb { R } )\) is an open subset of \(\mathbf { M } ( m \times n , \mathbb { R } )\) , and therefore is itself a smooth mn-dimensional manifold. A similar argument shows that \(\mathbf { M } _ { n } ( m \times n , \mathbb { R } )\) is a smooth mn-manifold when \(n < m\) Example 1.29 (Spaces of Linear Maps). Suppose V and W are finite-dimensional real vector spaces, and let \(\operatorname { L } ( V ; W )\)
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Matrices of Full Rank). The previous example has a natural generalization to rectangular matrices of full rank. By continuity of the determinant function, this same submatrix has nonzero determinant on a neighborhood of A in M ( m × n , ℝ ) , which implies that A has a neighborhood contained in M _m ( m × n , ℝ ) Thus, M _m ( m × n , ℝ ) is an open subset of M ( m × n , ℝ ) , and therefore is itself a smooth mn-dimensional manifold. A similar argument shows that M _n ( m × n , ℝ ) is a smooth mn-manifold when n < m // Mathlib has Lie-manifold infrastructure for units of normed algebras and continuous-linear-map spaces, but no checked bridge realizes Lee’s exact finite matrix GL(n,ℝ), full-rank rectangular-matrix open locus, or algebraic L(V,W) dimension bundle. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.29
shows that \(\mathbf { M } _ { n } ( m \times n , \mathbb { R } )\) is a smooth mn-manifold when \(n < m\) Example 1.29 (Spaces of Linear Maps). Suppose V and W are finite-dimensional real vector spaces, and let \(\operatorname { L } ( V ; W )\) denote the set of linear maps from V to W . Then because \(\operatorname { L } ( V ; W )\) is itself a finite-dimensional vector space (whose dimension is the product of the dimensions of V and W ), it has a natural smooth manifold structure as in Example 1.24. One way to put global coordinates on it is to choose bases for V and W , and represent each \(T \in \mathrm { L } ( V ; W )\) by its matrix, which yields an isomorphism of \(\operatorname { L } ( V ; W )\) with \(\mathbf { M } ( m \times n , \mathbb { R } )\) for \(m = \dim W\) and \(n = \dim V\) Example 1.30 (Graphs of Smooth Functions). If \(U \subseteq \mathbb { R } ^ { n }\) is an open subset and \(f \colon U \to \mathbb { R } ^ { k }\)
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Spaces of Linear Maps). Suppose V and W are finite-dimensional real vector spaces, and let L ( V ; W ) denote the set of linear maps from V to W . Then because L ( V ; W ) is itself a finite-dimensional vector space (whose dimension is the product of the dimensions of V and W ), it has a natural smooth manifold structure as in Example 1.24. One way to put global coordinates on it is to choose bases for V and W , and represent each T ∈ L ( V ; W ) by its matrix, which yields an isomorphism of L ( V ; W ) with M ( m × n , ℝ ) for m = dim W and n = dim V // Mathlib has Lie-manifold infrastructure for units of normed algebras and continuous-linear-map spaces, but no checked bridge realizes Lee’s exact finite matrix GL(n,ℝ), full-rank rectangular-matrix open locus, or algebraic L(V,W) dimension bundle. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.30
isomorphism of \(\operatorname { L } ( V ; W )\) with \(\mathbf { M } ( m \times n , \mathbb { R } )\) for \(m = \dim W\) and \(n = \dim V\) Example 1.30 (Graphs of Smooth Functions). If \(U \subseteq \mathbb { R } ^ { n }\) is an open subset and \(f \colon U \to \mathbb { R } ^ { k }\) is a smooth function, we have already observed above (Example 1.3) that the graph of f is a topological n-manifold in the subspace topology. Since \(\Gamma ( f )\) is covered by the single graph coordinate chart \(\varphi \colon \Gamma ( f ) \to U\) (the restriction of \(\pi _ { 1 } )\) , we can put a canonical smooth structure on \(\Gamma ( f )\) by declaring the graph coordinate chart \(( \Gamma ( f ) , \varphi )\) to be a smooth chart. Example 1.31 (Spheres). We showed in Example 1.4 that the n-sphere \(\mathbb { S } ^ { n } \subseteq \mathbb { R } ^ { n + 1 }\) is a topological n-manifold.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Graphs of Smooth Functions). If U ⊆ ℝ ^n is an open subset and f : U → ℝ ^k is a smooth function, we have already observed above (Example 1.3) that the graph of f is a topological n-manifold in the subspace topology. Since Gamma ( f ) is covered by the single graph coordinate chart φ : Gamma ( f ) → U (the restriction of π _1 ) , we can put a canonical smooth structure on Gamma ( f ) by declaring the graph coordinate chart ( Gamma ( f ) , φ ) to be a smooth chart. // No checked graph-of-a-smooth-map manifold construction with Lee’s canonical graph-coordinate smooth structure was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.31
(Spheres). Example 1.4 showed that the \(n\)-sphere \(\mathbb{S}^{n} \subseteq \mathbb{R}^{n+1}\) is a topological \(n\)-manifold. The collection of charts \((U_{i}^{\pm}, \varphi_{i}^{\pm})\) is a smooth atlas, and so defines a smooth structure on \(\mathbb{S}^{n}\), called its standard smooth structure.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Spheres). We showed in Example 1.4 that the n-sphere mathbb S ^n ⊆ ℝ ^n + 1 is a topological n-manifold. Thus, the collection of charts ( U _i ^± , φ _i ^± ) is a smooth atlas, and so defines a smooth structure on overline mathbb S ^n . We call this its standard smooth structure. Mathlib’s sphere manifold is built from stereographic charts, not Lee’s graph-coordinate atlas, and no checked atlas-equivalence bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Convention/notation — standard smooth structure on the sphere
With the square root in the \(j\)th position, and a similar formula when \(i > j\); when \(i = j\) an even simpler computation gives \(\varphi_{i}^{+} \circ (\varphi_{i}^{-})^{-1} = \varphi_{i}^{-} \circ (\varphi_{i}^{+})^{-1} = \operatorname{Id}_{\mathbb{B}^{n}}\). Thus the collection of charts \((U_{i}^{\pm}, \varphi_{i}^{\pm})\) is a smooth atlas, and so defines a smooth structure on \(\mathbb{S}^{n}\), called its standard smooth structure.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (with the square root in the j th position), and a similar formula holds when i > j When i = j , an even simpler computation gives φ _i ^+ ∘ ( φ _i ^- ) ^- 1 = φ _i ^- ∘ ( φ _i ^+ ) ^- 1 = IdBn . Thus, the collection of charts ( U _i ^± , φ _i ^± ) is a smooth atlas, and so defines a smooth structure on overline mathbb S ^n . We call this its standard smooth structure. Mathlib’s sphere manifold is built from stereographic charts, not Lee’s graph-coordinate atlas, and no checked atlas-equivalence bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.32
(Level Sets). The preceding example can be generalized as follows. Because D φ ( a ) is a row matrix whose entries are the partial derivatives ( ∂ varPhi / ∂ x ^1 ( a ) , … , ∂ varPhi / ∂ x ^n ( a ) ) , for each a ∈ M there is some i such that ∂ varPhi / ∂ x ^i ( a ) ≠ 0 It follows from the implicit function theorem (Theorem C.40, with x ^i playing the role of y) that there is a neighborhood U _0 of a such that M ∩ U _0 can be expressed as a graph of an equation of the form x ^i = f (x ^1, … , widehat x ^i, … , x ^n ), for some smooth real-valued function f defined on an open subset of ℝ ^n - 1 . . For any c ∈ ℝ , the set φ ^- 1 ( c ) is called a level set of Phi . Therefore, arguing just as in the case of the n-sphere, we see that M is a topological manifold of dimension \(n-1\), with a smooth structure for which each graph coordinate chart is a smooth chart.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Level Sets). The preceding example can be generalized as follows. Because D φ ( a ) is a row matrix whose entries are the partial derivatives ( ∂ varPhi / ∂ x ^1 ( a ) , … , ∂ varPhi / ∂ x ^n ( a ) ) , for each a ∈ M there is some i such that ∂ varPhi / ∂ x ^i ( a ) ≠ 0 It follows from the implicit function theorem (Theorem C.40, with x ^i playing the role of y) that there is a neighborhood U _0 of a such that M ∩ U _0 can be expressed as a graph of an equation of the form x ^i = f (x ^1, … , widehat x ^i, … , x ^n ), for some smooth real-valued function f defined on an open subset of ℝ ^n - 1 . . For any c ∈ ℝ , the set φ ^- 1 ( c ) is called a level set of Phi . Therefore, arguing just as in the case of the n-sphere, we see that M is a topological Implicit/submersion machinery exists, but no checked regular-level-set theorem at the required interface was found that owns Lee’s stated smooth (n−1)-manifold conclusion. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.33
Example 1.33 (Projective Spaces). The n-dimensional real projective space \(\mathbb { R P } ^ { n }\) is a topological n-manifold by Example 1.5. Let us check that the coordinate charts \(( U _ { i } , \varphi _ { i } )\) constructed in that example are all smoothly compatible. Assuming for convenience that \(i > j\) , it is straightforward to compute that \[ \varphi_ {j} \circ \varphi_ {i} ^ {- 1} (u ^ {1}, \dots , u ^ {n}) = \left(\frac {u ^ {1}}{u ^ {j}}, \dots , \frac {u ^ {j - 1}}{u ^ {j}}, \frac {u ^ {j + 1}}{u ^ {j}}, \dots , \frac {u ^ {i - 1}}{u ^ {j}}, \frac {1}{u ^ {j}}, \frac {u ^ {i}}{u ^ {j}}, \dots , \frac {u ^ {n}}{u ^ {j}}\right), \] U _ { i } U _ { j } )$ to $_ {
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Projective Spaces). The n-dimensional real projective space mathbb R P ^n is a topological n-manifold by Example 1.5. Let us check that the coordinate charts ( U _i , φ _i ) constructed in that example are all smoothly compatible. Assuming for convenience that i > j , it is straightforward to compute that varphi_j ∘ varphi_i ^- 1 (u ^1, … , u ^n) = ((u ^1)/(u ^j), … , (u ^j - 1)/(u ^j), (u ^j + 1)/(u ^j), … , (u ^i - 1)/(u ^j), (1)/(u ^j), (u ^i)/(u ^j), … , (u ^n)/(u ^j) ), which is a diffeomorphism from φ _i ( U _i ∩ U _j ) to φ _j ( U _i ∩ U _j ) No checked real-projective-space smooth manifold with the standard quotient atlas was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.34
(Smooth Product Manifolds). If \(M_{1},\dots,M_{k}\) are smooth manifolds of dimensions \(n_{1},\dots,n_{k}\), Example 1.8 showed that the product space \(M_{1} \times \cdots \times M_{k}\) is a topological manifold of dimension \(n_{1}+\cdots+n_{k}\), with charts \((U_{1} \times \cdots \times U_{k},\ \varphi_{1} \times \cdots \times \varphi_{k})\). These charts define the product smooth manifold structure; for example, it yields a smooth structure on the \(n\)-torus \(\mathbb{T}^{n} = \mathbb{S}^{1} \times \cdots \times \mathbb{S}^{1}\).
Formalized. Mathlib/Geometry/Manifold/ChartedSpace.lean::prodChartedSpace, prodChartedSpace_chartAt; Mathlib/Geometry/Manifold/IsManifold/Basic.lean::IsManifold.prod, IsManifold.mem_maximalAtlas_prod; Mathlib/Analysis/InnerProductSpace/PiL2.lean::EuclideanSpace.finAddEquivProd — IsManifold.prod gives the natural product C^∞ structure and mem_maximalAtlas_prod puts products of smooth charts in its maximal atlas. EuclideanSpace.finAddEquivProd supplies the explicit ℝ^(n+m) ≃ ℝ^n×ℝ^m dimension bridge. Iteration gives Lee’s finite product construction.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Lemma 1.35
Lemma 1.35 (Smooth Manifold Chart Lemma). Let M be a set, and suppose we are given a collection \(\{ U _ { \alpha } \}\) of subsets of M together with maps ’ \(U _ { \alpha } \to \mathbb { R } ^ { n }\) , such that the following properties are satisfied: (i) For each ˛, \(\varphi _ { \alpha }\) is a bijection between \(U _ { \alpha }\) and an open subset \(\varphi _ { \alpha } ( U _ { \alpha } ) \subseteq \mathbb { R } ^ { n }\) (ii) For each ˛ and ˇ, the sets \(\varphi _ { \alpha } ( U _ { \alpha } \cap U _ { \beta } )\) and \(\varphi _ { \beta } ( U _ { \alpha } \cap U _ { \beta } )\) are open in \(\mathbb { R } ^ { n }\) (iii) Whenever \(U _ { \alpha } \cap U _ { \beta } \neq \emptyset\) , the map ’ˇ \(\circ \varphi _ { \alpha } ^ { - 1 } \colon \varphi _ { \alpha } ( U _ { \alpha } \cap U _ { \beta } ) \to \varphi _ { \beta } ( U _ { \alpha } \cap U _ { \beta } ) \ i s\) smooth. (iv) Countably many of the sets \(U _ { \alpha }\) cover M . (v) Whenever \(p , q\) are distinct points in M; either there exists some \(U _ { \alpha }\) containing both p and q or there exist disjoint sets \(U _ { \alpha } , U _ { \beta }\) with \(p \in U _ { \alpha }\) and \(q \in U _ { \beta }\) Then M has a unique smooth manifold structure such that each \(( U _ { \alpha } , \varphi _ { \alpha } )\) is a smooth chart. Fig. 1.9 The smooth manifold chart lemma Proof. We define the topology by taking all sets of the form \(\varphi _ { \alpha } ^ { - 1 } ( V )\) , with V an open subset of \(\mathbb { R } ^ { n }\) , as a basis. To prove that this is a basis for a topology, we example, this yields a smooth manifold structure on the n-torus \(\mathbb { T } ^ { n } = \mathbb { S } ^ { 1 } \times \cdots \times \mathbb { S } ^ { 1 }\) // In each of the examples we have seen so far, we constructed a smooth manifold structure in two stages: we started with a topological space and checked that it was a topological manifold, and then we specified a smooth structure.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Smooth Manifold Chart Lemma). Let M be a set, and suppose we are given a collection U _α of subsets of M together with maps ’ U _α → ℝ ^n , such that the following properties are satisfied: (i) For each ˛, φ _α is a bijection between U _α and an open subset φ _α ( U _α ) ⊆ ℝ ^n (ii) For each ˛ and ˇ, the sets φ _α ( U _α ∩ U _β ) and φ _β ( U _α ∩ U _β ) are open in ℝ ^n (iii) Whenever U _α ∩ U _β ≠ emptyset , the map ’ ˇ ∘ φ _α ^- 1 : φ _α ( U _α ∩ U _β ) → φ _β ( U _α ∩ U _β ) i s smooth. (iv) Countably many of the sets U _α cover M . (v) Whenever p , q are distinct points in M; either there exists some U _α containing both p and q or there exist disjoint sets U _α , U _β with p ∈ U _α and q ∈ U _β Then M has a unique smooth manifold structure such that each ( U _α , φ _α ) is a smooth chart. ChartedSpaceCore constructs a topology and charted space from partial equivalences with continuous transition maps, but no checked theorem bundles Lee’s smooth transition hypotheses plus his separation condition into the complete Smooth Manifold Chart Lemma. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Example 1.36
Example 1.36 (Grassmann Manifolds). Let V be an n-dimensional real vector space. For any integer \(0 \leq k \leq n\) , we let \(\mathbf { G } _ { k } ( V )\) denote the set of all k-dimensional linear subspaces of V . We will show that \(\mathbf { G } _ { k } ( V )\) can be naturally given the structure of a smooth manifold of dimension k \(( n - k )\) With this structure, it is called a Grassmann manifold, or simply a Grassmannian. In the special case \(V = \mathbb { R } ^ { n }\) , the Grassmannian \(\mathbf { G } _ { k } \left( \mathbb { R } ^ { n } \right)\) is often denoted by some simpler notation such as \(\mathrm { G } _ { k , n }\) or \(\mathbf { G } ( k , n )\) Note that \(\operatorname { G } _ { 1 } \left( \mathbb { R } ^ { n + 1 } \right)\) is exactly the n-dimensional projective space \(\mathbb { R P } ^ { n }\) The construction of a smooth structure on \(\operatorname { G } _ { k } ( V )\) is somewhat more involved than the ones we have done so far, but the basic idea is just to use linear algebra to construct To prove that this is a basis for a topology, we need to show that for any point \(p\) in the intersection of two basis sets \(\varphi _ { \alpha } ^ { - 1 } ( V )\) and \(\varphi _ { \beta } ^ { - 1 } ( W )\) there is a third basis set containing \(p\) and contained in the intersection.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Grassmann Manifolds). Let V be an n-dimensional real vector space. For any integer 0 ≤ k ≤ n , we let G _k ( V ) denote the set of all k-dimensional linear subspaces of V . We will show that G _k ( V ) can be naturally given the structure of a smooth manifold of dimension k ( n - k ) With this structure, it is called a Grassmann manifold, or simply a Grassmannian. In the special case V = ℝ ^n , the Grassmannian G _k ( ℝ ^n ) is often denoted by some simpler notation such as G _k , n or G ( k , n ) Note that G _1 ( ℝ ^n + 1 ) is exactly the n-dimensional projective space mathbb R P ^n Algebraic Grassmannians exist elsewhere in Mathlib, but no checked finite-dimensional real Grassmann manifold with dimension k(n-k) and Lee’s chart construction was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Convention/notation — source terminology/construction
We will use the notations Int ℍ ^n and ∂ ℍ ^n to denote the interior and boundary of ℍ ^n respectively, as a subset of ℝ ^n . When n > 0 , this means \[ \operatorname{Int}\mathbb{H}^{n} = \{(x^{1},\dots,x^{n}) \in \mathbb{R}^{n} : x^{n} > 0\}, \qquad \partial\mathbb{H}^{n} = \{(x^{1},\dots,x^{n}) \in \mathbb{R}^{n} : x^{n} = 0\}. \]
Formalized. Mathlib/Geometry/Manifold/Instances/Real.lean::EuclideanHalfSpace, range_modelWithCornersEuclideanHalfSpace, interior_range_modelWithCornersEuclideanHalfSpace, frontier_range_modelWithCornersEuclideanHalfSpace — EuclideanHalfSpace n is Mathlib’s closed half-space model. The cited range/interior/frontier lemmas identify the model range with {y | 0 ≤ y 0}, its interior with {y | 0 < y 0}, and its frontier with {y | y 0 = 0}, exactly Lee’s Int ℍ^n/∂ℍ^n convention.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/convention — chart for M
H } ^ { 0 } = $ An n-dimensional topological manifold with boundary is a second-countable Hausdorff space M in which every point has a neighborhood homeomorphic either to an open subset of \(\mathbb { R } ^ { n }\) or to a (relatively) open subset of \(\mathbb { H }\) (Fig. 1.11). An open subset $ M$ together with a map ’ \(U \to \mathbb { R } ^ { n }\) that is a homeomorphism onto an open subset of \(\mathbb { R } ^ { n }\) or \(\mathbb { H } ^ { n }\) will be called a chart for M , just as in the case of manifolds. When it is necessary to make the distinction, we will call \(( U , \varphi )\) an interior chart if \(\varphi ( U )\) is an open subset of \(\mathbb { R } ^ { n }\) (which includes the case of an open subset of \(\mathbb { H } ^ { n }\) that does not intersect \(\partial \mathbb { H } ^ { n } )\) , and a boundary chart if $ \(\mathbb { H } ^ { n }\) such that \(\varphi ( U ) \cap \partial \mathbb { H } ^ { n } \neq \emptyset\) chart whose image is a set of the form \(B _ { r } ( x ) \cap \mathbb { H } ^ { n }\)
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: An n-dimensional topological manifold with boundary is a second-countable Hausdorff space M in which every point has a neighborhood homeomorphic either to an open subset of ℝ ^n or to a (relatively) open subset of ℍ ^n (Fig. 1.11). An open subset U ⊆ M together with a map ’ U → ℝ ^n that is a homeomorphism onto an open subset of ℝ ^n or ℍ ^n will be called a chart for M , just as in the case of manifolds. When it is necessary to make the distinction, we will call ( U , φ ) an interior chart if φ ( U ) is an open subset of ℝ ^n (which includes the case of an open subset of ℍ ^n that does not intersect ∂ ℍ ^n ) , and a boundary chart if φ ( U ) is an open subset of ℍ ^n such that φ ( U ) ∩ ∂ ℍ ^n ≠ emptyset A boundary chart whose image is a set of the form B _r ( x ) ∩ ℍ ^n for some x ∈ ∂ ℍ ^n and r > 0 is called a coordinate half-ball. EuclideanHalfSpace, ChartedSpace, and the model 𝓡∂ n encode manifolds with boundary, but the row additionally classifies interior/boundary charts and coordinate half-balls; no checked whole-row interface owns all of those clauses. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Definition/convention — interior point of M
A point \(p \in M\) is an interior point of \(M\) if it lies in the domain of some interior chart, and a boundary point if it lies in the domain of a boundary chart sending \(p\) to \(\partial\mathbb{H}^{n}\). The boundary of \(M\), the set of all its boundary points, is denoted \(\partial M\); its interior, the set of all its interior points, is denoted \(\operatorname{Int} M\).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A point p ∈ M is called an interior point of M if it is in the domain of some interior chart. It is a boundary point of M if it is in the domain of a boundary chart that sends p to ∂ ℍ ^n . The boundary of M (the set of all its boundary points) is denoted by @M ; similarly, its interior, the set of all its interior points, is denoted by Int M . ModelWithCorners.IsInteriorPoint/IsBoundaryPoint give canonical preferred-chart predicates, but for merely topological manifolds Mathlib does not prove their equivalence with Lee’s existential arbitrary-chart definition; the chart-independence bridge is only available for C¹ and higher. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Theorem 1.37
Theorem 1.37 (Topological Invariance of the Boundary). If M is a topological manifold with boundary, then each point of M is either a boundary point or an interior point, but not both. Thus @M and Int M are disjoint sets whose union is M . F
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (Topological Invariance of the Boundary). If M is a topological manifold with boundary, then each point of M is either a boundary point or an interior point, but not both. Thus @M and Int M are disjoint sets whose union is M . isInteriorPoint_or_isBoundaryPoint is available for the preferred-chart model predicate, but Mathlib explicitly notes that chart-independence for finite-dimensional topological manifolds requires singular homology and is not proved there. Hence Lee’s Topological Invariance of the Boundary is not credited. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Definition/convention — source terminology/construction
Be careful to observe the distinction between these new definitions of the terms boundary and interior and their usage to refer to the boundary and interior of a subset of a topological space. A manifold with boundary may have nonempty boundary in this new sense, irrespective of whether it has a boundary as a subset of some other topological space. If we need to emphasize the difference between the two notions of boundary, we will use the terms topological boundary and manifold boundary as appropriate. For example, the closed unit ball \({ \overline { { \mathbb { B } } } } ^ { n }\) is a manifold with boundary (see Problem 1-11), whose manifold boundary is \(\mathbb { S } ^ { n - 1 }\) . Its topological boundary as a subset of \(\mathbb { R } ^ { n }\) happens to be the sphere as well. However, if we think of \({ \overline { { \mathbb { B } } } } ^ { n }\) as a topological space in its own right, then as a subset of itself, it has empty topological boundary. And if we think of it as a subset of \(\mathbb { R } ^ { n + 1 }\) (considering \(\mathbb { R } ^ { n }\) as a subset of \(\mathbb { R } ^ { n + 1 }\) in the obvious way), its topological boundary is all of \({ \overline { { \mathbb { B } } } } ^ { n }\) . Note that \(\mathbb { H } ^ { n }\) is itself a manifold with boundary, and its manifold boundary is the same as its topological boundary as a subset of \(\mathbb { R } ^ { n }\) . Every interval in \(\mathbb { R }\) is a 1-manifold with boundary, whose manifold boundary consists of its endpoints.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Be careful to observe the distinction between these new definitions of the terms boundary and interior and their usage to refer to the boundary and interior of a subset of a topological space. A manifold with boundary may have nonempty boundary in this new sense, irrespective of whether it has a boundary as a subset of some other topological space. If we need to emphasize the difference between the two notions of boundary, we will use the terms topological boundary and manifold boundary as appropriate. For example, the closed unit ball overline mathbb B ^n is a manifold with boundary (see Problem 1-11), whose manifold boundary is mathbb S ^n - 1 . Its topological boundary as a subset of ℝ ^n happens to be the sphere as well. However, if we think of overline mathbb B ^n as a topological space in its own right, then as a subset of itself, it has empty topological boundary. And if we think of it as a subset of ℝ ^n + 1 (considering ℝ ^n as a subset of ℝ ^n + 1 in the obvious way), its topological boundary is all of overline mathbb B ^n . Note that ℍ ^n is itself a manifold with boundary, and its manifold boundary is the same as its topological boundary as a subset of ℝ ^n . Every interval in ℝ is a 1-manifold with boundary, whose manifold boundary consists of its endpoints (if any). This is a warning distinguishing manifold boundary from ambient set-theoretic boundary; no distinct checked owner is required. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Definition/convention — source terminology/construction
with boundary is a manifold if and only if its boundary is empty (see Proposition 1.38 below). Even though the term manifold with boundary encompasses manifolds as well, we will often use redundant phrases such as manifold without boundary if we wish to emphasize that we are talking about a manifold in the original sense, and manifold with \(o r\) without boundary to refer to a manifold with boundary if we wish emphasize that the boundary might be empty. (The latter phrase will often appear when our primary interest is in manifolds, but the results being discussed are just as easy to state and prove in the more general case of manifolds with boundary.) Note that the word “manifold” without further qualification always means a manifold without boundary. In the literature, you will also encounter the terms closed manifold to mean a compact manifold without boundary, and open manifold to mean a noncompact manifold without boundary. <d
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Even though the term manifold with boundary encompasses manifolds as well, we will often use redundant phrases such as manifold without boundary if we wish to emphasize that we are talking about a manifold in the original sense, and manifold with o r without boundary to refer to a manifold with boundary if we wish emphasize that the boundary might be empty. (The latter phrase will often appear when our primary interest is in manifolds, but the results being discussed are just as easy to state and prove in the more general case of manifolds with boundary.) Note that the word “manifold” without further qualification always means a manifold without boundary. In the literature, you will also encounter the terms closed manifold to mean a compact manifold without boundary, and open manifold to mean a noncompact manifold without boundary. Boundaryless-manifold terminology exists, but the source row is primarily nomenclature and no exact standalone declaration matches the full wording. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Proposition 1.38
Let M be a topological n-manifold with boundary. (a) Int M is an open subset of M and a topological n-manifold without boundary. (b) ∂M is a closed subset of M and a topological (n−1)-manifold without boundary. (c) M is a topological manifold if and only if ∂M=∅. (d) If n=0, then ∂M=∅ and M is a 0-manifold.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let M be a topological n-manifold with boundary. (a) Int M is an open subset of M and a topological n-manifold without boundary. (b) ∂M is a closed subset of M and a topological (n−1)-manifold without boundary. (c) M is a topological manifold if and only if ∂M=∅. (d) If n=0, then ∂M=∅ and M is a 0-manifold. InteriorBoundary.lean proves openness/closedness and boundary chart-independence for C¹ manifolds, and its comments explicitly note the finite-dimensional topological result is not yet proved. It also lacks the full (n−1) topological-manifold boundary theorem required here. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Proposition 1.40
Let M be a topological manifold with boundary. (a) M has a countable basis of precompact coordinate balls and half-balls. (b) M is locally compact. (c) M is paracompact. (d) M is locally path-connected. (e) M has countably many components, each of which is an open subset of M and a connected topological manifold with boundary. (f) The fundamental group of M is countable.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let M be a topological manifold with boundary. (a) M has a countable basis of precompact coordinate balls and half-balls. (b) M is locally compact. (c) M is paracompact. (d) M is locally path-connected. (e) M has countably many components, each of which is an open subset of M and a connected topological manifold with boundary. (f) The fundamental group of M is countable. Pinned manifold infrastructure supplies local compactness, local path-connectedness and generic paracompactness, but the row also requires the precompact coordinate ball/half-ball basis, component package, and countability of π₁; no checked whole-row owner was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Definition/convention — smooth
To see how to define a smooth structure on a manifold with boundary, recall that a map from an arbitrary subset \(A \subseteq \mathbb { R } ^ { n }\) to \(\mathbb { R } ^ { k }\) is said to be smooth if in a neighborhood of each point of A it admits an extension to a smooth map defined on an open subset of \(\mathbb { R } ^ { n }\) (see Appendix C, p. 645). Thus, if U is an open subset of \(\mathbb { H } ^ { n }\) , a map \(F \colon U \to \mathbb { R } ^ { k }\) is smooth if for each \(x \in U\) , there exists an open subset \(\widetilde { U } \subseteq \mathbb { R } ^ { n }\) containing x and a smooth map \(\widetilde { F } \colon \widetilde { U } \to \mathbb { R } ^ { k }\) that agrees with \(F\) on \({ \widetilde { U } } \cap \mathbb { H } ^ { n }\) (Fig. 1.12). If F is such a map, the restriction of F to U Int \(\mathbb { H } ^ { n }\) is smooth in the usual sense. By continuity, all partial derivatives of F at points of \(U \cap \partial \mathbb { H } ^ { n }\) are determined by their values in Int H, and therefore in particular are independent of the choice of extension. It is a fact (which we will neither prove nor use) that \(F \colon U \to \mathbb { R } ^ { k }\) is smooth in this sense if and only if F is continuous, \(F | _ { U \cap \mathrm { I n t } \mathbb { H } ^ { n } }\) is smooth, and the partial derivatives of \(F | _ { U \cap { \mathrm { I n t } } \mathbb { H } ^ { n } }\) of all orders have continuous extensions to all of U . (One direction is obvious; the other direction depends on a lemma of Émile Borel, which shows that there is a smooth function def be empty.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: To see how to define a smooth structure on a manifold with boundary, recall that a map from an arbitrary subset A ⊆ ℝ ^n to ℝ ^k is said to be smooth if in a neighborhood of each point of A it admits an extension to a smooth map defined on an open subset of ℝ ^n (see Appendix C, p. 645). Thus, if U is an open subset of ℍ ^n , a map F : U → ℝ ^k is smooth if for each x ∈ U , there exists an open subset tilde(U) ⊆ ℝ ^n containing x and a smooth map tilde(F) : tilde(U) → ℝ ^k that agrees with F on tilde(U) ∩ ℍ ^n (Fig. 1.12). If F is such a map, the restriction of F to U Int ℍ ^n is smooth in the usual sense. By continuity, all partial derivatives of F at points of U ∩ ∂ ℍ ^n are determined by their values in Int H n , and therefore in particular are independent of the choice of extension. It is a fact (which we will neither prove nor use) that F : U → ℝ ^k is smooth in this sense if and only if F is continuous, F ∣ U ∩ I n t ℍ ^n is smooth, and the partial derivatives of F ∣ U ∩ I n t ℍ ^n of all orders have continuous extensions to all of U . (One direction is obvious; the other direction depends on a lemma of Émile Borel, which shows that there is a smooth function defined in the lower half-space whose derivatives all match those of F on U ∩ ∂ ℍ ^n . See, e.g., [Hör90, Thm. 1.2.6].) ContDiffWithinAt formalizes smoothness relative to a set via local Taylor-series data, not Lee’s local-extension definition; no checked equivalence to the extension criterion (including the all-orders boundary derivative clause/Borel converse) was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Definition/convention — smooth manifold
\(\partial g / \partial y \to \infty\) as \(y 0\) Thus \(g\) is not smooth on \(U\) Now let M be a topological manifold with boundary. As in the manifold case, a smooth structure for M is defined to be a maximal smooth atlas—a collection of charts whose domains cover M and whose transition maps (and their inverses) are smooth in the sense just described. With such a structure, M is called a smooth manifold with boundary. Every smooth manifold is automatically a smooth manifold with boundary (whose boundary is empty).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Now let M be a topological manifold with boundary. As in the manifold case, a smooth structure for M is defined to be a maximal smooth atlas—a collection of charts whose domains cover M and whose transition maps (and their inverses) are smooth in the sense just described. With such a structure, M is called a smooth manifold with boundary. Every smooth manifold is automatically a smooth manifold with boundary (whose boundary is empty). IsManifold (𝓡∂ n) ∞ M and maximal-atlas machinery formalize smooth manifolds with boundary, but no checked bridge realizes Lee’s additional claim that every boundaryless smooth 𝓡 n-manifold is automatically the corresponding 𝓡∂ n-manifold with empty boundary. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Definition/convention — smooth chart for M
If \(M\) is a smooth manifold with boundary, any chart in the given smooth atlas is a smooth chart for \(M\), and smooth coordinate balls, smooth coordinate half-balls and regular coordinate balls are defined as for smooth manifolds. A subset \(B \subseteq M\) is a regular coordinate half-ball if there is a smooth coordinate half-ball \(B' \supseteq \overline{B}\) and a smooth coordinate map \(\varphi \colon B' \to \mathbb{H}^{n}\) such that, for some \(r' > r > 0\), \[ \varphi(B) = B_{r}(0) \cap \mathbb{H}^{n}, \quad \varphi(\overline{B}) = \overline{B}_{r}(0) \cap \mathbb{H}^{n}, \quad\text{and}\quad \varphi(B') = B_{r'}(0) \cap \mathbb{H}^{n}. \]
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Just as for smooth manifolds, if M is a smooth manifold with boundary, any chart in the given smooth atlas is called a smooth chart for M . Smooth coordinate balls, smooth coordinate half-balls, and regular coordinate balls in M are defined in the obvious ways. In addition, a subset B ⊆ M is called a regular coordinate half-ball if there is a smooth coordinate half-ball B ^prime supseteq bar(B) and a smooth coordinate map ’ B ^prime → ℍ ^n such that for some r ^prime > r > 0 we have Smooth boundary charts are formalized through the model-with-corners atlas, but coordinate ball/half-ball and regular coordinate half-ball terminology are not packaged by a checked declaration. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and unbridged alternative representations.
Proposition 1.45
Suppose \(M_{1},\dots,M_{k}\) are smooth manifolds and \(N\) is a smooth manifold with boundary. Then \(M_{1} \times \cdots \times M_{k} \times N\) is a smooth manifold with boundary, and \(\partial(M_{1} \times \cdots \times M_{k} \times N) = M_{1} \times \cdots \times M_{k} \times \partial N\).
Formalized. Mathlib/Geometry/Manifold/IsManifold/Basic.lean::IsManifold.prod; Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean::BoundarylessManifold.prod, ModelWithCorners.boundary_of_boundaryless_left, ModelWithCorners.boundary_prod — IsManifold.prod constructs the smooth product. BoundarylessManifold.prod iterates the boundaryless factors, and boundary_of_boundaryless_left states literally that when the left factor is boundaryless, ∂(M×N)=M×∂N; iterating gives Lee’s formula for finitely many M_i and one manifold-with-boundary N.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 1.46
Theorem 1.46 (Smooth Invariance of the Boundary). Suppose M is a smooth manifold with boundary and \(p \in M\) . If there is some smooth chart \(( U , \varphi )\) for M such that \(\varphi ( U ) \subseteq \mathbb { H } ^ { n }\) and \(\varphi ( p ) \in \partial \mathbb { H } ^ { n }\) , then the same is true for every smooth chart whose domain contains domains cover M and whose transition maps (and their inverses) are smooth in the sense just described.
Formalized. Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean::ModelWithCorners.isBoundaryPoint_iff_of_mem_atlas, ModelWithCorners.isInteriorPoint_iff_of_mem_atlas — For a C^1 (hence smooth) manifold, isBoundaryPoint_iff_of_mem_atlas says that the canonical boundary-point predicate is equivalent to being sent to the model frontier by any atlas chart containing the point. Applying the equivalence to the assumed chart and then to an arbitrary smooth chart is exactly Lee’s smooth invariance-of-boundary theorem.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0