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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 55 definitions, 7 theorems, 21 propositions, 4 lemmas, 1 corollary, 5 examples, 5 constructions and 3 conventions.

Of the 101 statements checked against Lean, 54 are formalized somewhere and 47 are not.

Status	Statements	Share	What it means
in Mathlib	54	53%	Mathlib states and proves it.
not formalized	47	47%	A documented search found no Lean statement of it anywhere.
checked in total	101

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Appendix A, FC08-CA-U001–FC08-CA-U101, exactly 101 unique contiguous rows from the canonical FC08 unit catalogue.
Search order: project A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0; Lean 4.33.0), current upstream H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0; Lean 4.34.0-rc2), then indexed/current/external Lean search. Existing FC02/FC07 topology mappings were used only as search leads; every cited Mathlib file was revalidated at exact P before promotion.
Result: 54 pinned mathlib rows and 47 dated unmatched rows. Positive IDs: U001, U002, U004, U005, U007, U008, U010, U011, U012, U014, U015, U016, U017, U018, U019, U020, U021, U022, U025, U029, U030, U031, U032, U033, U038, U039, U040, U042, U047, U049, U051, U056, U060, U061, U063, U065, U067, U069, U070, U075, U076, U077, U078, U080, U081, U082, U083, U084, U085, U088, U093, U096, U097, U101.
The strongest direct matches are native topology/metric/basis/subspace/quotient definitions, the exact CompactExhaustion structure and construction, native homotopy/path-class/fundamental-group objects, and the pinned covering lifting criterion.
Lee’s special “neighborhood = open neighborhood” convention is not conflated with Mathlib’s generic neighborhood-filter membership. nhds_basis_opens is used only where an open-neighborhood basis itself is the source object.
Large bundled propositions (subspace/product/disjoint-union/quotient/connectedness/compactness properties) remain unmatched when Mathlib only supplies the clauses separately. Likewise Lee’s definition of a proper map allows discontinuous maps, whereas Mathlib IsProperMap includes continuity; U073 is therefore not identified with it. U077 is mapped only because the source assumes continuity and a locally compact Hausdorff target, so the compact-preimage characterization bridges to IsProperMap.
FC07’s TauCeti reference-port evidence was reconsidered for U098–U100, but no short compatible bridge from Lee’s locally-simply-connected convention to the later package’s universal-cover hypotheses plus the full uniqueness statement was found; these rows remain unmatched rather than silently changing hypotheses.
N=2026-09-07 marks all negative decisions; strict whole-row semantics apply uniformly.

Definition/convention — open subsets

FC08-CA-U001 · Appendix A, § Topological Spaces; source L17896 · in Mathlib

Let $X$ be a set. A topology on $X$ is a collection $\mathcal{T}$ of subsets of $X$, called open subsets, such that (i) $X$ and $\emptyset$ are open; (ii) the union of any family of open subsets is open; and (iii) the intersection of any finite family of open subsets is open. A pair $(X,\mathcal{T})$ is called a topological space.

Formalized. Mathlib/Topology/Defs/Basic.lean::TopologicalSpace, IsOpen — TopologicalSpace is exactly a family of open sets closed under arbitrary unions and finite intersections; IsOpen names membership in it.

Definition/convention — topological space

FC08-CA-U002 · Appendix A, § Topological Spaces; source L17904 · in Mathlib

consisting of a set X together with a topology on X is called a topological space. Ordinarily, when the topology is understood, one omits mention of it and simply says “X is a topological space.”

Formalized. Mathlib/Topology/Defs/Basic.lean::TopologicalSpace — A TopologicalSpace X is precisely Lee’s topology datum on the underlying type.

Definition/convention — neighborhood of p

FC08-CA-U003 · Appendix A, § Topological Spaces; source L17910 · not formalized

A neighborhood of p is an open subset containing p. Similarly, a neighborhood of the set S is an open subset containing S. (Be warned that some authors use the word “neighborhood” in the more general sense of a subset containing an open subset containing p or S.)

Not formalized. none; no complete checked declaration under strict bundle semantics — Lee intentionally reserves “neighborhood” for an open set containing the point/set; Mathlib’s generic neighborhood notion is filter membership and includes nonopen supersets. nhds_basis_opens gives the canonical open basis but does not identify the two terminology conventions. Strict whole-row semantics reject partial clause coverage and unbridged reconstruction.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — closed

FC08-CA-U004 · Appendix A, § Topological Spaces; source L17912 · in Mathlib

S is said to be closed if $X \setminus S$ is open (where $X \setminus S$ denotes the set difference $\{ x \in X : x \not \in S \} )$

Formalized. Mathlib/Topology/Defs/Basic.lean::IsClosed — IsClosed s is defined by openness of the complement, exactly Lee’s convention.

Definition/convention — source terminology/construction

FC08-CA-U005 · Appendix A, § Topological Spaces; source L17914 · in Mathlib

The interior of S , denoted by Int S, is the union of all open subsets of X contained in S.

Formalized. Mathlib/Topology/Defs/Basic.lean::interior — interior s is the greatest open subset of s, equivalently the union of all open subsets contained in s.

Definition/convention — source terminology/construction

FC08-CA-U006 · Appendix A, § Topological Spaces; source L17916 · not formalized

The exterior of S , denoted by Ext S, is the union of all open subsets of X contained in $X \setminus S$

Not formalized. none; no complete checked declaration under strict bundle semantics — The source packages a named relative/exterior construction in a convention not represented by one checked declaration with the same interface; it is expressible from interior/complement or subtype topology, but that expression would be reconstruction. Strict whole-row semantics reject partial clause coverage and unbridged reconstruction.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — source terminology/construction

FC08-CA-U007 · Appendix A, § Topological Spaces; source L17918 · in Mathlib

The closure of S , denoted by bar(S) , , is the intersection of all closed subsets of X containing S.

Formalized. Mathlib/Topology/Defs/Basic.lean::closure — closure s is the least closed superset of s, equivalent to Lee’s intersection-of-all-closed-supersets definition.

Definition/convention — source terminology/construction

FC08-CA-U008 · Appendix A, § Topological Spaces; source L17920 · in Mathlib

The boundary of S , denoted by @S, is the set of all points of X that are in neither Int S nor E

Formalized. Mathlib/Topology/Defs/Basic.lean::frontier; Mathlib/Topology/Closure.lean::frontier_eq_inter_compl_interior — frontier is Lee’s boundary; frontier_eq_inter_compl_interior identifies it exactly with points in neither the interior nor the exterior.

Definition/convention — an isolated point of S

FC08-CA-U009 · Appendix A, § Topological Spaces; source L17922 · not formalized

A point $p \in S$ is an isolated point of $S$ if $p$ has a neighborhood $U \subseteq X$ with $U \cap S = \{p\}$.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — a limit point of S

FC08-CA-U010 · Appendix A, § Topological Spaces; source L17924 · in Mathlib

point $p \in X$ (not necessarily in S ) is said to be a limit point of S if every neighborhood of p contains at least one point of S other than p.

Formalized. Mathlib/Topology/ClusterPt.lean::accPt_iff_nhds — For the principal filter of S, accPt_iff_nhds says every neighborhood contains a distinct point of S, exactly Lee’s limit-point condition.

Definition/convention — dense in X

FC08-CA-U011 · Appendix A, § Topological Spaces; source L17926 · in Mathlib

S is said to be dense in X if ${ \overline { { S } } } = X$ , or equivalently if every nonempty open subset of X contains at least one point ed on the theory of timedependent flows (see Theorem 9.48).

Formalized. Mathlib/Topology/Closure.lean::Dense, dense_iff_closure_eq, dense_iff_inter_open — Mathlib gives both source characterizations: closure equal to the whole space and intersection with every nonempty open set.

Definition/convention — nowhere dense in X

FC08-CA-U012 · Appendix A, § Topological Spaces; source L17928 · in Mathlib

S is said to be nowhere dense in X if Sx contains no nonempty open s

Formalized. Mathlib/Topology/GDelta/Basic.lean::IsNowhereDense — IsNowhereDense s is defined by interior (closure s) = ∅, exactly the source convention.

Definition/convention — next

FC08-CA-U013 · Appendix A, § Topological Spaces; source L17930 · not formalized

The most important concepts of topology are continuous maps and convergent sequences, which we define next. Let X and Y be topological compute the derivative of a tensor field under a flow.

Not formalized. none; no complete checked declaration under strict bundle semantics — This is transitional prose rather than a mathematical theorem/construction with an independent checked owner. Strict whole-row semantics reject partial clause coverage and unbridged reconstruction.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — continuous

FC08-CA-U014 · Appendix A, § Topological Spaces; source L17932 · in Mathlib

map $F \colon X \to Y$ is said to be continuous if for every open subset $U \subseteq Y$ , the preimage $F ^ { - 1 } ( U )$ is open flows.

Formalized. Mathlib/Topology/Defs/Basic.lean::Continuous — Continuous f is the open-preimage condition.

Definition/convention — homeomorphism

FC08-CA-U015 · Appendix A, § Topological Spaces; source L17934 · in Mathlib

A continuous bijective map $F \colon X \to Y$ with continuous inverse is a homeomorphism, and $X$ and $Y$ are homeomorphic if such a map exists.

Formalized. Mathlib/Topology/Homeomorph/Defs.lean::Homeomorph — Homeomorph X Y is a bijection with continuous forward and inverse maps, exactly the source object.

Definition/convention — a local homeomorphism

FC08-CA-U016 · Appendix A, § Topological Spaces; source L17936 · in Mathlib

A continuous map $F \colon X \to Y$ is a local homeomorphism if every $p \in X$ has a neighborhood $U \subseteq X$ such that $F(U)$ is open in $Y$ and $F$ restricts to a homeomorphism from $U$ onto $F(U)$.

Formalized. Mathlib/Topology/IsLocalHomeomorph.lean::IsLocalHomeomorph, isLocalHomeomorph_iff_isOpenEmbedding_restrict — The pointwise open-restriction characterization is exactly Lee’s local-homeomorphism definition.

Convention/notation — source terminology/construction

FC08-CA-U017 · Appendix A, § Topological Spaces; source L17938 · in Mathlib

Given a sequence $( { \boldsymbol { p } } _ { i } ) _ { i = 1 } ^ { \infty }$ of points in X and a point $p \in X$ , the sequence is said to converge to p if for every neighborhood U of $p _ { : }$ , there exists a positive integer N such that $p _ { i } \in U$ for all $i \geq N$ . In this case, we write $p _ { i } \to p$ or $\scriptstyle \operatorname* { l i m } _ { i \to \infty } p _ { i } = p$ Exercise A.1. Let $F \colon X \to Y$ be a map between topological spaces. Prove that each of the following conditions is equivalent to continuity.

Formalized. Mathlib/Topology/Defs/Filter.lean::Tendsto; Mathlib/Topology/Neighborhoods.lean::nhds_basis_opens — Convergence of a sequence is Tendsto u atTop (𝓝 p); the open-neighborhood basis expands this to Lee’s eventual-membership formulation.

Example A.4

FC08-CA-U018 · Appendix A, § Topological Spaces; source L17958 · in Mathlib

Example A.4 (Discrete Spaces). If X is an arbitrary set, the discrete topology on X is the topology defined by declaring every subset of X to be open. Any space that has the discrete topology is called a discrete space.

Formalized. Mathlib/Topology/Order.lean::DiscreteTopology — DiscreteTopology X is exactly the topology in which every subset is open.

Example A.5

FC08-CA-U019 · Appendix A, § Topological Spaces; source L17960 · in Mathlib

Example A.5 (Metric Spaces). A metric space is a set M endowed with a distance function (also called a metric) d $M \times M \to \mathbb { R }$ (where R denotes the set of rea numbers) satisfying the following properties for all $x , y , z \in M$ (i) POSITIVITY: $d ( x , y ) \geq 0$ , with equality if and only if $x = y$ (ii) SYMMETRY: $d ( x , y ) = d ( y , x )$ (iii) TRIANGLE INEQUALITY: $d ( x , z ) \leq d ( x , y ) + d ( y , z )$ If M is a metric space, $x \in M$ ; and $r > 0$ , the open ball of radius r around x is the set \[ B _ {r} (x) = \left\{y \in M: d (x, y) < r \right\}, \] and the closed ball of radius r is \[ \bar {B} _ {r} (x) = \left\{y \in M: d (x, y) \leq r \right\}. \] The metric topology on M is defined by declaring a subset $S \subseteq M$ to be open if for every point $x \in S$ , there is some $r > 0$ such t

Formalized. Mathlib/Topology/MetricSpace/Defs.lean::MetricSpace; Mathlib/Topology/MetricSpace/Pseudo/Defs.lean::Metric.ball, Metric.closedBall, Metric.nhds_basis_ball — The metric axioms, open/closed balls, and the ball basis for the induced metric topology directly realize the full example.

Definition/convention — source terminology/construction

FC08-CA-U020 · Appendix A, § Topological Spaces; source L17986 · in Mathlib

If S is a nonempty bounded subset of M; the diameter of S is the number diam $S = \operatorname* { s u p } \{ d ( x , y ) : x , y \in S \}$

Formalized. Mathlib/Topology/MetricSpace/Bounded.lean::Metric.diam — Metric.diam is the supremum of pairwise distances on a set, with Lee’s bounded nonempty regime as its ordinary finite-valued case.

Definition/convention — source terminology/construction

FC08-CA-U021 · Appendix A, § Topological Spaces; source L17988 · in Mathlib

A sequence $(x_{i})_{i=1}^{\infty}$ in a metric space $M$ is a Cauchy sequence if for every $\varepsilon > 0$ there is an integer $N$ such that $i, j \geq N$ implies $d(x_{i},x_{j}) < \varepsilon$.

Formalized. Mathlib/Topology/UniformSpace/Cauchy.lean::CauchySeq — For metric spaces, CauchySeq unfolds to the usual ε-eventual pairwise-distance definition.

Definition/convention — complete

FC08-CA-U022 · Appendix A, § Topological Spaces; source L17990 · in Mathlib

A metric space M is said to be complete if every Cauchy sequence in M converges to a point of M .

Formalized. Mathlib/Topology/UniformSpace/Cauchy.lean::CompleteSpace — CompleteSpace asserts that every Cauchy filter/sequence converges; in metric spaces it is equivalent to Lee’s sequence definition.

Example A.6

FC08-CA-U023 · Appendix A, § Topological Spaces; source L17992 · not formalized

(Euclidean Spaces). For each integer $n \geq 1$, the set $\mathbb{R}^{n}$ of ordered $n$-tuples of real numbers is $n$-dimensional Euclidean space. A point is written $(x^{1},\dots,x^{n})$, $(x^{i})$, or $x$, and the numbers $x^{i}$ are its components or coordinates; for small $n$ the traditional names $(x,y,z)$ are often used. Coordinates carry superscripts rather than subscripts, for consistency with the Einstein summation convention. By convention $\mathbb{R}^{0}$ is the one-element set $\{0\}$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has Euclidean/normed-space instances and many of the listed facts separately, but this source row bundles Lee’s coordinate conventions or several Euclidean identifications/examples; no single checked interface owns the whole bundle. Strict whole-row semantics reject partial clause coverage and unbridged reconstruction.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — Euclidean norm

FC08-CA-U024 · Appendix A, § Topological Spaces; source L17994 · not formalized

For each $x \in \mathbb{R}^{n}$, the Euclidean norm of $x$ is the nonnegative real number \[ |x| = \sqrt{(x^{1})^{2} + \cdots + (x^{n})^{2}}, \] and for $x, y \in \mathbb{R}^{n}$ the Euclidean distance function is $d(x,y) = |x-y|$.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — Euclidean distance

FC08-CA-U025 · Appendix A, § Topological Spaces; source L18000 · in Mathlib

For $x, y \in \mathbb{R}^{n}$, the Euclidean distance function is $d(x,y) = |x-y|$.

Formalized. Mathlib/Analysis/Normed/Group/Basic.lean::dist_eq_norm — dist_eq_norm is exactly d(x,y)=‖x-y‖ in the norm-induced Euclidean metric.

Convention/notation — Euclidean topology

FC08-CA-U026 · Appendix A, § Topological Spaces; source L18006 · not formalized

This distance function turns $\mathbb { R } ^ { n }$ into a complete metric space. The resulting metric topology on $\mathbb { R } ^ { n }$ is called the Euclidean

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Example A.7

FC08-CA-U027 · Appendix A, § Topological Spaces; source L18008 · not formalized

Example A.7 (Complex Euclidean Spaces). We also sometimes have occasion to work with complex Euclidean spaces. We consider the set C of complex numbers, as a set, to be simply $\mathbb { R } ^ { 2 }$ , with the complex number $x + i y$ corresponding to $( x , y ) \in \mathbb { R } ^ { 2 }$ . For any positive integer n, the n-dimensional complex Euclidean space is the set $\mathbb { C } ^ { n }$ of ordered n-tuples of complex numbers. It becomes a topological space when identified with $\mathbb { R } ^ { 2 { \bar { n } } }$ via the correspondence \[ \left(x ^ {1} + i y ^ {1}, \dots , x ^ {n} + i y ^ {n}\right) \leftrightarrow \left(x ^ {1}, y ^ {1}, \dots , x ^ {n}, y ^ {n}\right).\tag{//} \]

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Example A.8

FC08-CA-U028 · Appendix A, § Topological Spaces; source L18014 · not formalized

Example A.8 (Subsets of Euclidean Spaces). Every subset of $\mathbb { R } ^ { n }$ or $\mathbb { C } ^ { n }$ becomes a metric space, and thus a topological space, when endowed with the Euclidean metric. Whenever we mention such a subset, it is always assumed to have this metric topology unless otherwise specified. It is a complete metric space if and only if it is a closed subset of $\mathbb { R } ^ { n }$ . Here are some standard subsets of Euclidean spaces that we work with frequently: The unit interval is the subset $I \subseteq \mathbb { R }$ defined by \[ I = [ 0, 1 ] = \{x \in \mathbb {R}: 0 \leq x \leq 1 \}. \] The (open) unit ball of dimension n is the subset $\mathbb { B } ^ { n } \subseteq \mathbb { R } ^ { n }$ defined by \[ \mathbb {B} ^ {n} = \left\{x \in \mathbb {R} ^ {n}: | x | < 1 \right\}. \] The closed unit ball of dimension n is the subset $\overline { { \mathbb { B } } } ^ { n } \subseteq \mathbb { R } ^ { n }$ defined by \[ \overline {{\mathbb {B}}} ^ {n} = \left\{x \in \mathbb {R} ^ {n}: | x | \leq 1 \right\}. \] The terms (open) unit disk and closed unit disk are commonly used for $\mathbb { B } ^ { 2 }$ and ${ \overline { { \mathbb { B } } } } ^ { 2 }$ , respectively. For $n \geq 0$ , the (unit) n-sphere is the subset $\mathbb { S } ^ { n } \subseteq \mathbb { R } ^ { n + 1 }$ defined by \[ \mathbb {S} ^ {n} = \left\{x \in \mathbb {R} ^ {n + 1}: | x | = 1 \right\}. \] Sometimes it is useful to think of an odd-dimensional sphere $\mathbb { S } ^ { 2 n + 1 }$ as a subset of $\mathbb { C } ^ { n + 1 }$ , by means of the usual identification of $\mathbb { C } ^ { n + 1 }$ with $\mathbb { R } ^ { 2 n + 2 }$ The (unit) circle is the 1-sphere $\mathbb { S } ^ { 1 }$ , considered either as a subset of $\mathbb { R } ^ { 2 }$ or as a subset of C. ## Hausdorff Spaces Topological spaces allow us to describe a wide variety of concepts of “spaces.” But for the purposes of manifold theory, arbitrary topological spaces are far too general, because they can have some unpleasant properties, as the next exercise illustrates.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — a Hausdorff space

FC08-CA-U029 · Appendix A, § Hausdorff Spaces; source L18052 · in Mathlib

To avoid pathological cases like this, which result when X does not have sufficiently many open subsets, we often restrict our attention to topological spaces satisfying the following special condition. A topological space X is said to be a Hausdorff space if for every pair of distinct points $p , q \in X$ , there exist disjoint open subsets $U , V \subseteq X$ such that $p \in U$ and $q \in V .$

Formalized. Mathlib/Topology/Separation/Hausdorff.lean::T2Space — T2Space is exactly pairwise separation of distinct points by disjoint neighborhoods/open sets.

Definition/convention — a basis for the topology of X

FC08-CA-U030 · Appendix A, § Bases and Countability; source L18060 · in Mathlib

Suppose X is a topological space. A collection of open subsets of X is said to be a basis for the topology of X (plural: bases) if every open subset of X is the union of some collection of elements simple compactness argument shows that there is some neighborhood $U _ { 1 } \subseteq U$ of $p _ { 0 }$ such that $\omega _ { t }$ is nondegenerate on $U _ { 1 }$ for all $t \in { \overline { { J } } }$ .

Formalized. Mathlib/Topology/Bases.lean::IsTopologicalBasis — IsTopologicalBasis B is precisely the source condition that open sets are unions of basis elements.

Definition/convention — topology generated by B

FC08-CA-U031 · Appendix A, § Bases and Countability; source L18062 · in Mathlib

More generally, suppose X is merely a set, and is a collection of subsets of X satisfying the following conditions: (i) $\begin{array} { r } { X = \bigcup _ { B \in \mathcal { B } } B . } \end{array}$ (ii) $\mathrm { I f ~ } B _ { 1 } , B _ { 2 } \in \mathcal { B }$ and $x \in B _ { 1 } \cap B _ { 2 }$ , then there exists $B _ { 3 } \in { \mathcal { B } }$ such that $x \in B _ { 3 } \subseteq$ $B _ { 1 } \cap B _ { 2 } .$ Then the collection of all unions of elements of is a topology on X, called the topology generated by , and i

Formalized. Mathlib/Topology/Bases.lean::IsTopologicalBasis — Mathlib’s basis-generation API formalizes the cover/refinement criterion and identifies the resulting topology as the topology generated by the basis.

Definition/convention — topology generated by B

FC08-CA-U032 · Appendix A, § Bases and Countability; source L18068 · in Mathlib

Then the collection of all unions of elements of B is a topology on X, called the topology generated by B , and B is a basis for this topology.

Formalized. Mathlib/Topology/Bases.lean::IsTopologicalBasis.eq_generateFrom — A topological basis generates exactly the ambient topology; this is Lee’s generated-topology convention.

Definition/convention — neighborhood basis at p

FC08-CA-U033 · Appendix A, § Bases and Countability; source L18070 · in Mathlib

If X is a topological space and $p \in X$ a neighborhood basis at p is a collection $\mathcal { B } _ { p }$ of neighborhoods of p such that every neighborhood of p contains at least one $B \in { \mathcal { B } } _ { p } .$

Formalized. Mathlib/Topology/Neighborhoods.lean::nhds_basis_opens; Mathlib/Order/Filter/Bases/Basic.lean::Filter.HasBasis — nhds_basis_opens says open sets containing p form a basis of 𝓝 p; Filter.HasBasis is exactly the refinement property Lee calls a neighborhood basis.

Definition/convention — countably infinite

FC08-CA-U034 · Appendix A, § Bases and Countability; source L18072 · not formalized

A set is said to be countably infinite if it admits a bijection with the set of positive integers, and countable if it is finite or countably infinite. A topological space X is said to be first-countable if there is a countable neighborhood basis at each point, and second-countable if there is a countable basis for its topology. Since a countable basis for X contains a countable neighborhood basis at each point, secondcountability implies first-countability.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has the constituent countability/filter/sequence/cover notions, but this source row bundles several definitions or several sequential characterizations. No one declaration or short checked assembly owns all clauses under strict whole-row semantics. Strict whole-row semantics reject partial clause coverage and unbridged reconstruction.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — sequence

FC08-CA-U035 · Appendix A, § Bases and Countability; source L18074 · not formalized

The next lemma expresses the most important properties of first-countable spaces. To say that a sequence is eventually in a subset means that all but finitely many terms of the sequence are in the subset. L

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Lemma A.12

FC08-CA-U036 · Appendix A, § Bases and Countability; source L18076 · not formalized

Lemma A.12 (Sequence Lemma). Let X be a first-countable space, let $A \subseteq X$ be any subset, and let $x \in X$ (a) $x \in { \overline { { A } } }$ if and only if x is a limit of a sequence of points in A. (b) $x \in$ Int A if and only if every sequence in X converging to x is eventually in A. (c) A is closed in X if and only if A contains every limit of every convergent sequence of points in A. (d) A is open in X if and only if every sequence in X converging to a point of A is eventually in $A$.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — open cover

FC08-CA-U037 · Appendix A, § Bases and Countability; source L18092 · not formalized

One of the most important properties of second-countable spaces is expressed in the following proposition. Let X be a topological space. A cover of X is a collection of subsets of X whose union is X; it is called an open cover if each of the sets in is open. A subcover of is a subcollection of that is still a cover. P

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Proposition A.16

FC08-CA-U038 · Appendix A, § Bases and Countability; source L18094 · in Mathlib

Proposition A.16. Let X be a second-countable topological space. Every open cover of X has a countable subcover.

Formalized. Mathlib/Topology/Compactness/Lindelof.lean::SecondCountableTopology.toHereditarilyLindelof, IsLindelof.elim_countable_subcover — Second-countability supplies Lindelöfness, whose elimination theorem gives a countable subcover of every open cover.

Definition/convention — relative topology) by declaring a subset U

FC08-CA-U039 · Appendix A, § Subspaces; source L18102 · in Mathlib

Probably the simplest way to obtain new topological spaces from old ones is by taking subsets of other spaces. If X is a topological space and $S \subseteq X$ is an arbitrary subset, we define the subspace topology on S (sometimes called the relative topology) by declaring a subset $U \subseteq S$ to be open in S if and only if there exists an open subset V X such that $U = V \cap S$ A subset of S that is open or closed in the subspace topology is sometimes said to be relatively open or relatively closed in S , to make it clear that we do not mean open or closed as a subset of X. Any subset of X endowed with the subspace topology is said to be a subspace of X . Whenever we treat a subset of a topological space as a space in its own right, we always assume that it has the subspace topology unless otherwise specified.

Formalized. Mathlib/Topology/Defs/Induced.lean::TopologicalSpace.induced; Mathlib/Topology/Constructions.lean::isOpen_induced_iff — The subtype topology is the induced topology and isOpen_induced_iff gives exactly the intersection-with-an-ambient-open-set characterization.

Definition/convention — topological embedding

FC08-CA-U040 · Appendix A, § Subspaces; source L18104 · in Mathlib

If X and Y are topological spaces, a continuous injective map $F \colon X \to Y$ is called a topological embedding if it is a homeomorphism onto its image $F ( X ) \subseteq Y$ in the subspace topolo the level set of f .

Formalized. Mathlib/Topology/Defs/Induced.lean::Topology.IsEmbedding — IsEmbedding f is injective and inducing; equivalently a continuous injection that is a homeomorphism onto its range with the subspace topology.

Proposition A.17

FC08-CA-U041 · Appendix A, § Subspaces; source L18108 · not formalized

Proposition A.17 (Properties of the Subspace Topology). Let X be a topological space and let S be a subspace of X. (a) CHARACTERISTIC PROPERTY: If Y is a topological space, a map F Y S is continuous if and only if the composition $\iota _ { S } \circ F \colon Y \to X$ is continuous, where $\iota _ { S } \colon S \hookrightarrow$ X is the inclusion map (the restriction of the identity map of X to S ). (b) The subspace topology is the unique topology on S for which the characteristic property holds. (c) A subset $K \subseteq S$ is closed in S if and only if there exists a closed subset $L \subseteq X$ such that $K = L \cap S$ (d) The inclusion map $\iota _ { S } \colon S \hookrightarrow X$ is a topological embedding. (e) If Y is a topological space and $F \colon X \to Y$ is continuous, then $F | _ { S } \colon S \to Y$ (the restriction of F to S ) is continuous. (f) If is a basis for the topology of X , then $\mathcal { B } _ { S } = \{ B \cap S : B \in \mathcal { B } \}$ is a basis for the subspace topology on S. (g) If X is Hausdorff, then so is S . (h) If X is first-countable, then so is S . (i)

Not formalized. none; no complete checked declaration under strict bundle semantics — The underlying subspace/product/disjoint-union infrastructure is formalized, but this row is a multi-clause construction/properties bundle (or tagged-image convention) not owned in full by one declaration or a short assembly. Strict whole-row semantics reject partial clause coverage and unbridged reconstruction.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Lemma A.19

FC08-CA-U042 · Appendix A, § Subspaces; source L18132 · in Mathlib

Lemma A.19 (Continuity Is Local). Continuity is a local property, in the following sense: if F X Y is a map between topological spaces such that every poin $p \in X$ has a neighborhood U on which the restriction $F | _ { U }$ is continuous, then F is continuous.

Formalized. Mathlib/Topology/ContinuousOn.lean::continuous_of_cover_nhds — continuous_of_cover_nhds is the local-to-global continuity theorem on a neighborhood cover, exactly Lee’s lemma.

Lemma A.20

FC08-CA-U043 · Appendix A, § Subspaces; source L18134 · not formalized

Lemma A.20 (Gluing Lemma for Continuous Maps). Let X and Y be topological spaces, and suppose one of the following conditions holds: (a) $B _ { 1 } , \ldots , B _ { n }$ are finitely many closed subsets of X whose union is X. (b) $\{ B _ { i } \} _ { i \in A }$ is a collection of open subsets of X whose union is X. Suppose that for all i we are given continuous maps $F _ { i } \colon B _ { i } \to Y$ that agree on overlaps: $F _ { i } | _ { B _ { i } \cap B _ { j } } = F _ { j } | _ { B _ { i } \cap B _ { j } }$ . Then there exists a unique continuous map $F \colon X \to Y$ whose restriction to each $B _ { i }$ is equal ding the definitions, we find that $\eta = d f$ A symplectic manifold $( M , \omega )$ together with a smooth function $H \in C ^ { \infty } ( M )$ is called a Hamiltonian system.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Construction/definition — source terminology/construction

FC08-CA-U044 · Appendix A, § Product Spaces; source L18148 · not formalized

If $X_{1},\dots,X_{k}$ are finitely many sets, their Cartesian product is the set $X_{1} \times \cdots \times X_{k}$ of ordered $k$-tuples $(x_{1},\dots,x_{k})$ with $x_{i} \in X_{i}$ for each $i$. The $i$th projection map is $\pi_{i} \colon X_{1} \times \cdots \times X_{k} \to X_{i}$, $\pi_{i}(x_{1},\dots,x_{k}) = x_{i}$.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Construction/definition — product topology

FC08-CA-U045 · Appendix A, § Product Spaces; source L18150 · not formalized

subsets of $X _ { 1 } \times$ $\cdots \times X _ { k }$ of the form $U _ { 1 } U _ { k } $ , where each $U _ { i }$ is open in $X _ { i } ,$ , forms a basis for a topology on $X _ { 1 } \times \cdots \times X _ { k }$ , called the product topology. Endowed with this topology, a finite product of topological spaces is called a product space. Any open subset of the form $U _ { 1 } \times \cdots \times U _ { k } \subseteq X _ { 1 } \times \cdots \times X _ { k }$ , where each $U _ { i }$ is open in $X _ { i } ,$ , is called a product open subset. (A slightly different definition is required for products of infinitely many spaces, but we need only the finite case. See [LeeTM] for more about infinite product spaces.)

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Proposition A.23

FC08-CA-U046 · Appendix A, § Product Spaces; source L18152 · not formalized

spaces.) Proposition A.23 (Properties of the Product Topology). Suppose $X _ { 1 } , \ldots , X _ { k }$ are topological spaces, 1 } X _ { k }$ be their product space. (a) CHARACTERISTIC PROPERTY: If B is a topological space, a map $ $X _ { 1 } \times \cdots \times X _ { k }$ is continuous if and only if each of its component functions { i } =$ $\pi _ { i } \circ F \colon B X _ { i }$ is continuous. (b) The product topology is the unique topology on $ i $X _ { 1 } \times \cdots \times X _ { k } X _ { i }$ is continuous. (d) Given any continuous maps $F _ { i } \colon X _ { i } Y _ { i }$ X _ { k } Y _ { 1 } , x _ {k}) = (F _ {1} (x _ {1}), , F _ {k} (x _ {k}) ). \[ (e) $I f S _ { i }$ is a subspace of X for $i = 1 , \ldots , n$ , the product topology and the subspace topology on $S _ { 1 } \times \cdots \times S _ { n } \subseteq X _ { 1 } \times \cdots \times X _ { n }$ coincide. (f) For any $i \in \{ 1 , \ldots , k \}$ and any choices of points $a _ { j } \in X _ { j }$ for $j \neq i$ , the map $x \mapsto ( a _ { 1 } , \ldots , a _ { i - 1 } , x , a _ { i + 1 } , \ldots , a _ { k } )$ is a topological embedding of $X _ { i }$ into the product space $X _ { 1 } \times \cdots \times X _ { k } .$ (g) ${ \cal I f B } _ { i }$ is a basis for the topology of $X _ { i } f o r i = 1 , \ldots , k$ , then the collection \] {B} = {B _ {1} B _ {k}: B _ {i} \[ is a basis for the topology of $X _ { 1 } \times \cdots \times X _ { k } .$ (h) Every finite product of Hausdorff spaces is Hausdorff. (i) Every finite product of first-countable spaces is first-countable. (j) Every finite product of second-countable spaces is second-countable. Exercise A.24. Prove the preceding proposition. ## Disjoint Union Spaces Another simple way of building new topological spaces is by taking disjoint unions of other spaces. From a set-theoretic point of view, the disjoint union is defined as follows. If $( X _ { \alpha } ) _ { \alpha \in A }$ is an indexed family of sets, their disjoint union is the set \]

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — source terminology/construction

FC08-CA-U047 · Appendix A, § Disjoint Union Spaces; source L18188 · in Mathlib

Another simple way of building new topological spaces is by taking disjoint unions of other spaces. From a set-theoretic point of view, the disjoint union is defined as follows. If ( X _α ) _α ∈ A is an indexed family of sets, their disjoint union is the set \[ \coprod_{\alpha \in A} X_{\alpha} = \{(x,\alpha) : \alpha \in A,\ x \in X_{\alpha}\}, \] with canonical injections $\iota_{\alpha} \colon X_{\alpha} \to \coprod_{\alpha \in A} X_{\alpha}$.

Formalized. Mathlib/Data/Sigma/Basic.lean::Sigma — The dependent sum Σ a, X a is exactly the tagged disjoint union of an indexed family.

Convention/notation — source terminology/construction

FC08-CA-U048 · Appendix A, § Disjoint Union Spaces; source L18194 · not formalized

For each $\alpha ,$ there is a canonical injective map $\iota _ { \alpha } \colon X _ { \alpha } \to \coprod _ { \alpha \in A } X _ { \alpha }$ given by $\iota _ { \alpha } ( x ) =$ $( x , \alpha )$ , and the images of these maps for different values of ˛ are disjoint. Typically, we implicitly identify $X _ { \alpha }$ with its image in the disjoint union, thereby viewing $X _ { \alpha }$ as a subset of $\operatorname { I I } _ { \alpha \in A } X _ { \alpha }$ . The ˛ in the notation $( x , \alpha )$ should be thought of as $\mathbf { a \Sigma ^ { } } \mathrm { t a g ^ { \prime } }$ to indicate which set x comes from, so that the subsets corresponding to different values of ˛ are disjoint, even if some or all of the original sets $X _ { \alpha }$ were identical. Given an indexed family of topological spaces $( X _ { \alpha } ) _ { \alpha \in A }$ , we define the disjoint union topology on $\mathrm { U } _ { \alpha \in A } X _ { \alpha }$ by declaring a subset of $\mathrm { H } _ { \alpha \in A } X _ { \alpha }$ to be open if and only if its intersection with each $\overline { { X _ { \alpha } } }$ is open in ${ \overline { { X _ { \alpha } . } } }$

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Construction/definition — disjoint union topology

FC08-CA-U049 · Appendix A, § Disjoint Union Spaces; source L18196 · in Mathlib

Given an indexed family of topological spaces $( X _ { \alpha } ) _ { \alpha \in A }$ , we define the disjoint union topology on $\mathrm { U } _ { \alpha \in A } X _ { \alpha }$ by declaring a subset of $\mathrm { H } _ { \alpha \in A } X _ { \alpha }$ to be open if and only if its intersection with each $\overline { { X _ { \alpha } } }$ is open in ${ \overline { { X _ { \alpha } . } } }$ Proposition A.25 (Properties of the Disjoint Union Topology). Suppos

Formalized. Mathlib/Topology/Constructions.lean::isOpen_sigma_iff — isOpen_sigma_iff says a set in a dependent sum is open iff every tagged component preimage is open, exactly the disjoint-union topology.

Proposition A.25

FC08-CA-U050 · Appendix A, § Disjoint Union Spaces; source L18198 · not formalized

(Properties of the Disjoint Union Topology). Suppose $(X_{\alpha})_{\alpha \in A}$ is an indexed family of topological spaces and $\coprod_{\alpha \in A} X_{\alpha}$ carries the disjoint union topology. (a) Characteristic property: a map $F \colon \coprod_{\alpha \in A} X_{\alpha} \to Y$ is continuous if and only if $F \circ \iota_{\alpha} \colon X_{\alpha} \to Y$ is continuous for each $\alpha \in A$. (b) The disjoint union topology is the unique topology with that property. (c) A subset is closed if and only if its intersection with each $X_{\alpha}$ is closed. (d) Each injection $\iota_{\alpha} \colon X_{\alpha} \to \coprod_{\alpha \in A} X_{\alpha}$ is a topological embedding. (e) A disjoint union of Hausdorff spaces is Hausdorff. (f) A disjoint union of first-countable spaces is first-countable. (g) A disjoint union of countably many second-countable spaces is second-countable.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Construction/definition — quotient map

FC08-CA-U051 · Appendix A, § Quotient Spaces and Quotient Maps; source L18224 · in Mathlib

If X is a topological space, Y is a set, and $\pi \colon X \to Y$ is a surjective map, the quotient topology on Y determined by is defined by declaring a subset $U \subseteq Y$ to be open if and only if $\pi ^ { - 1 } ( U )$ is open in X. If X and Y are topological spaces, a map $\pi \colon X \to Y$ is called a quotient map if it is surjective and continuous and Y has the quotient topology determi are subject to constraints, as are the constituent particles of a rigid body, for example, then the configuration space is typically a submanifold of $\mathbb { R } ^ { 3 n }$ rather than an open subset.

Formalized. Mathlib/Topology/Defs/Induced.lean::Topology.IsQuotientMap — IsQuotientMap is surjectivity plus the coinduced/quotient topology, hence exactly Lee’s quotient-map package.

Definition/convention — equivalence relation

FC08-CA-U052 · Appendix A, § Quotient Spaces and Quotient Maps; source L18226 · not formalized

The following construction is the most common way of producing quotient maps. A relation on a set X is called an equivalence relation if it is reflexive $( x \sim x$ for all $x \in X )$ , symmetric $( x \sim y$ implies $y \sim x )$ , and transitive $( x \sim y$ and $y \sim z$ imply $x \sim z )$ . If $R \subseteq X \times X$ is any relation on X, then the intersection of all equivalence relations on $X$ containing R is an equivalence relation, called the equivalence relation generated by R. If is an equivalence relation on $X$ , then for each $x \in X$ , the equivalence class of x, denoted by Œx, is the set of all $y \in X$ such that $y \sim x$ . The set of all equivalence classes is a partition of X : a collection of disjoint nonempty subsets whose union is X .

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has quotient/setoid/open/closed-map infrastructure, but this row bundles generated equivalence relations, adjunction examples, saturation, several quotient properties, or quotient-space uniqueness beyond the single directly mapped universal property. No complete owner was found. Strict whole-row semantics reject partial clause coverage and unbridged reconstruction.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Construction/definition — quotient space (

FC08-CA-U053 · Appendix A, § Quotient Spaces and Quotient Maps; source L18228 · not formalized

Suppose $X$ is a topological space and $\sim$ is an equivalence relation on $X$. Let $X/\!\sim$ be the set of equivalence classes and $\pi \colon X \to X/\!\sim$ the natural projection. With the quotient topology determined by $\pi$, the space $X/\!\sim$ is the quotient space, or identification space, of $X$ determined by $\sim$. For example, if $X$ and $Y$ are topological spaces, $A \subseteq Y$ is closed and $f \colon A \to X$ is continuous, the relation $a \sim f(a)$ for $a \in A$ generates an equivalence relation on $X \sqcup Y$ whose quotient space $X \cup_{f} Y$ is called an adjunction space, formed by attaching $Y$ to $X$ along $f$.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — saturated

FC08-CA-U054 · Appendix A, § Quotient Spaces and Quotient Maps; source L18230 · not formalized

If $\pi \colon X \to Y$ is a map, a subset $U \subseteq X$ is said to be saturated with respect to if U is the entire preimage of its image: $U = \pi ^ { - 1 } { \bigl ( } \pi ( U ) { \bigr ) }$ . Given $y \in Y$ , the fiber of over y is the set $\pi ^ { - 1 } ( y )$ Thus, a subset of X is saturated if and only if it is a union of fibers.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Theorem A.27

FC08-CA-U055 · Appendix A, § Quotient Spaces and Quotient Maps; source L18232 · not formalized

Theorem A.27 (Properties of Quotient Maps). Let $\pi \colon X \to Y$ be a quotient map. (a) CHARACTERISTIC PROPERTY: If B is a topological space, a map $F \colon Y B$ is continuous if and only if F $\pi \colon X \to B$ is continuous. (b) The quotient topology is the unique topology on Y for which the characteristic property holds. (c) A subset $K \subseteq Y$ is closed if and only $i f \pi ^ { - 1 } ( K )$ is closed in X . (d) If is injective, then it is a homeomorphism. (e) $I f U \subseteq X$ is a saturated open or closed subset, then the restriction $\pi | _ { U } \colon U \to$ .U / is a quotient map. (f) Any composition of with another quotient map is again a quotient map.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Theorem A.30

FC08-CA-U056 · Appendix A, § Quotient Spaces and Quotient Maps; source L18258 · in Mathlib

Theorem A.30 (Passing to the Quotient). Suppose $\pi \colon X \to Y$ is a quotient map, B is a topological space, and $F \colon X \to B$ is a continuous map that is constant on the fibers of $( i . e . , \pi ( p ) = \pi ( q )$ implies $F ( p ) = F ( q ) )$ . Then there exists a unique continuous map $\widetilde { F } \colon Y \to B$ such that $F = \widetilde { F } \circ \pi$ Proof. The existence and uniqueness of $\widetilde { F }$ follow from set-theoretic considerations, and its continuity }} f = - [ X _ {g}, X _ {h} ] f = - X _ {g} X _ {h} f + X _ {h} X _ {g} f \ & = - X _ {g} {f, h } + X _ {h} {f, g } = - {{f, h }, g } + {{f, g }, h } \ & = - {g, {h, f } } - {h, {f, g } }.

Formalized. Mathlib/Topology/ContinuousMap/Basic.lean::Topology.IsQuotientMap.lift, Topology.IsQuotientMap.lift_comp, Topology.IsQuotientMap.liftEquiv — For a continuous map constant on fibers, lift descends it uniquely through a quotient map and lift_comp gives the required factorization; liftEquiv packages uniqueness.

Theorem A.31

FC08-CA-U057 · Appendix A, § Quotient Spaces and Quotient Maps; source L18262 · not formalized

(Uniqueness of Quotient Spaces). If $\pi_{1} \colon X \to Y_{1}$ and $\pi_{2} \colon X \to Y_{2}$ are quotient maps constant on each other’s fibers — that is, $\pi_{1}(p) = \pi_{1}(q)$ if and only if $\pi_{2}(p) = \pi_{2}(q)$ — then there is a unique homeomorphism $\varphi \colon Y_{1} \to Y_{2}$ with $\varphi \circ \pi_{1} = \pi_{2}$.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — an open map

FC08-CA-U058 · Appendix A, § Open and Closed Maps; source L18268 · not formalized

A map $F \colon X \to Y$, continuous or not, is an open map if $F(U)$ is open in $Y$ for every open $U \subseteq X$, and a closed map if $F(K)$ is closed in $Y$ for every closed $K \subseteq X$. Continuous maps may be open, closed, both or neither.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Theorem A.38

FC08-CA-U059 · Appendix A, § Open and Closed Maps; source L18288 · not formalized

Theorem A.38. Suppose X and Y are topological spaces, and $F \colon X \to Y$ is a continuous map that is either open or closed. (a) If F is surjective, then it is a quotient map. (b) If F is injective, then it is a topological embedding. (c) If F is bijective, then it is a homeomor M that is contained in a single level set of H , and the Hamiltonian vector field $X _ { H }$ is nowhere tangent to .

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — disconnected

FC08-CA-U060 · Appendix A, § Connectedness and Compactness; source L18302 · in Mathlib

Compactness A topological space X is said to be disconnected if it has two disjoint nonempty open subsets whose union is X, and it is connected otherwise. Equivalently, X is connected if and only if the only subsets of X that are both open and closed are and X itself. If X is any topological space, a connected subset of X is a subset that is a connected space when endowed with the subspace topology. For example, the nonempty connected subsets of R are the singletons (one-element sets) and the intervals, which are the subsets $J \subseteq \mathbb { R }$ containing more than one point and having the property that whenever $a , b \in J$ and $a < c < b$ , it follows that $c \in J$ as w

Formalized. Mathlib/Topology/Connected/Basic.lean::IsPreconnected, IsConnected; Mathlib/Topology/Order/IntermediateValue.lean::isPreconnected_iff_ordConnected — Mathlib’s connectedness is the no-open-separation condition; on the real line, isPreconnected_iff_ordConnected identifies connected subsets with order-convex intervals, with singletons included.

Definition/convention — component (

FC08-CA-U061 · Appendix A, § Connectedness and Compactness; source L18304 · in Mathlib

A maximal connected subset of X (i.e., a connected subset that is not properly contained in any larger connected subset) is called a component (or connected component)

Formalized. Mathlib/Topology/Connected/Basic.lean::connectedComponent — connectedComponent x is the maximal connected subset through x, exactly the source component.

Proposition A.39

FC08-CA-U062 · Appendix A, § Connectedness and Compactness; source L18306 · not formalized

Proposition A.39 (Properties of Connected Spaces). Let X and Y be topological spaces. (a) $I f F \colon X \to Y$ is continuous and X is connected, then $F ( X )$ is connected. (b) Every connected subset of X is contained in a single component of X. (c) A union of connected subspaces of X with a point in common is connected. (d) The components of X are disjoint nonempty closed subsets whose union is X, and thus they form a partition of X . (e) If S is a subset of X that is both open and closed, then S is a union of components of X . (f) Every finite product of connected spaces is connected. (g) Every quotient space of a connected space is conn n the same level set of H as $\varGamma$ ## Contact Structures As we have seen, symplectic manifolds must be even-dimensional; but there is a closely related structure called a contact structure that one can define on odddimensional manifolds.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib contains many constituent connectedness/compactness/properness facts, but the source row is a substantial multi-clause theorem or uses Lee’s compact-preimage definition of properness for maps not assumed continuous. No one checked owner matches the complete row. Strict whole-row semantics reject partial clause coverage and unbridged reconstruction.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — path-connected

FC08-CA-U063 · Appendix A, § Connectedness and Compactness; source L18324 · in Mathlib

Closely related to connectedness is path connectedness. If X is a topological space and $p , q \in X$ , a path in X from p to q is a continuous map $f \colon I \to X$ (where $I = [ 0 , 1 ] )$ such that $f ( 0 ) = p$ and $f ( 1 ) = q$ . If for every pair of points $p , q \in X$ there exists a path in X from p to q, then X is said to be path-connected. The path components of X are its maximal path-connected subse ooth 1-form $\theta$ with the property that for each $p \in M$ the restriction of $d \theta _ { p }$ to the subspace Ker $\theta _ { p } \subseteq T _ { p } M$ is nondegenerate, which is to say it is a symplectic tensor.

Formalized. Mathlib/Topology/Path.lean::Path; Mathlib/Topology/Connected/PathConnected.lean::IsPathConnected, pathComponent — Mathlib directly formalizes paths on [0,1], path-connected subsets, and maximal path components.

Proposition A.41

FC08-CA-U064 · Appendix A, § Connectedness and Compactness; source L18326 · after FC08-CA-U062 · not formalized

Proposition A.41 (Properties of Path-Connected Spaces). (a) Proposition A.39 holds with “connected” replaced by “path-connected” and “component” by “path component” throughout. (b) Every path-connected space is connected.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — locally path-connected

FC08-CA-U065 · Appendix A, § Connectedness and Compactness; source L18334 · in Mathlib

For most topological spaces we treat in this book, including all manifolds, connectedness and path connectedness turn out to be equivalent. The link between the two concepts is provided by the following notion. A topological space is said to be locally path-connected if it admits a basis of path-connected open subsets.

Formalized. Mathlib/Topology/Connected/LocallyPathConnected.lean::LocallyPathConnectedSpace, isOpen_isPathConnected_basis — The class is characterized by an open path-connected neighborhood basis, exactly Lee’s definition.

Proposition A.43

FC08-CA-U066 · Appendix A, § Connectedness and Compactness; source L18336 · not formalized

Proposition A.43 (Properties of Locally Path-Connected Spaces). Let X be a locally path-connected topological space. (a) The components of X are open in X. (b) The path components of X are equal to its components. (c) X is connected if and only if it is path-connected. (d) Every open subset of X is locally path-connected.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — compact

FC08-CA-U067 · Appendix A, § Connectedness and Compactness; source L18348 · in Mathlib

A topological space X is said to be compact if every open cover of X has a finite subcover. A compact subset of a topological space is one that is a compact space in the subspace topology. For example, it is a consequence of the Heine–Borel theorem that a subset of R is compact if and only if it is closed and bounded.

Formalized. Mathlib/Topology/Defs/Filter.lean::IsCompact; Mathlib/Topology/Compactness/Compact.lean::isCompact_iff_finite_subcover; Mathlib/Topology/MetricSpace/Bounded.lean::isCompact_iff_isClosed_bounded — Mathlib’s finite-subcover characterization is the source compactness definition, and its Heine–Borel theorem gives the stated closed-and-bounded criterion in Euclidean proper metric spaces.

Proposition A.45

FC08-CA-U068 · Appendix A, § Connectedness and Compactness; source L18350 · not formalized

Proposition A.45 (Properties of Compact Spaces). Let X and Y be topological spaces. (a) If $F \colon X \to Y$ is continuous and X is compact, then F .X / is compact. (b) If X is compact and f X R is continuous, then f is bounded and attains its maximum and minimum values on X. (c) Any union of finitely many compact subspaces of X is compact. (d) If X is Hausdorff and K and L are disjoint compact subsets of X, then there exist disjoint open subsets U; $V \subseteq X$ such that $K \subseteq U$ and $L \subseteq V$ (e) Every closed subset of a compact space is compact. (f) Every compact subset of a Hausdorff space is closed. (g) Every compact subset of a metric space is bounded. (h) Every finite product of compact spaces is compact. (i) Every quotient of a compact space is compact.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — Lipschitz constant for F

FC08-CA-U069 · Appendix A, § Connectedness and Compactness; source L18372 · in Mathlib

For maps between metric spaces, there are several variants of continuity that are useful, especially in the context of compact spaces. Suppose $( M _ { 1 } , d _ { 1 } )$ and $( M _ { 2 } , d _ { 2 } )$ are metric spaces, and $F \colon M _ { 1 } \to M _ { 2 }$ is a map. Then F is said to be uniformly continuous if for every $\varepsilon > 0 .$ , there exists $\delta > 0$ such that for all x; $y \in M _ { 1 } , d _ { 1 } ( x , y ) < \delta$ implies $d _ { 2 } \big ( F ( x ) , F ( y ) \big ) < \varepsilon .$ . It is said to be Lipschitz continuous if there is a constant C such that $d _ { 2 } \bigl ( F ( x ) , F ( y ) \bigr ) \leq C d _ { 1 } ( x , y )$ for all $x , y \in M _ { 1 }$ . Any such C is called a Lipschitz constant for F . We say that F is locally Lipschitz continuous if every point $x \in M _ { 1 }$ has a neighborhood on which F is Lipschitz continuous. (To emphasize the distinction, Lipschitz continuous functions are sometimes called uniformly or globally Lipsc

Formalized. Mathlib/Topology/UniformSpace/Defs.lean::UniformContinuous; Mathlib/Topology/EMetricSpace/Lipschitz.lean::LipschitzWith, LocallyLipschitz — These are exactly the uniform-continuity, global Lipschitz, and local Lipschitz predicates in Lee’s metric-space formulation.

Proposition A.48

FC08-CA-U070 · Appendix A, § Connectedness and Compactness; source L18376 · in Mathlib

Proposition A.48. Suppose $( M _ { 1 } , d _ { 1 } )$ and $( M _ { 2 } , d _ { 2 } )$ are metric spaces and $F \colon M _ { 1 } \to$ $M _ { 2 }$ is a map. Let K be any compact subset of $M _ { 1 }$ (a) If F is continuous, then $F | _ { K }$ is uniformly continuous. (b) If F is locally Lipschitz continuous, then $F | _ { K }$ is Lipschitz continuous.

Formalized. Mathlib/Topology/UniformSpace/HeineCantor.lean::IsCompact.uniformContinuousOn_of_continuous; Mathlib/Topology/Algebra/MetricSpace/Lipschitz.lean::LocallyLipschitzOn.exists_lipschitzOnWith_of_compact — The first theorem is Heine–Cantor on a compact set; the second states exactly that locally Lipschitz on a compact set admits one global Lipschitz constant there.

Proposition A.50

FC08-CA-U071 · Appendix A, § Connectedness and Compactness; source L18396 · not formalized

Proposition A.50 (Equivalent Formulations of Compactness). Suppose M is a second-countable Hausdorff space or a metric space. The following are equivalent. (a) M is compact. (b) Every infinite subset of M has a limit point in M . (c) Every sequence in M has a convergent subsequence in M . E

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Lemma A.52

FC08-CA-U072 · Appendix A, § Connectedness and Compactness; source L18408 · not formalized

Lemma A.52 (Closed Map Lemma). Suppose X is a compact space, Y is a Hausdorff space, and F X Y is a continuous map. (a) F is a closed map. (b) If F is surjective, it is a quotient map. (c) If F is injective, it is a topological embedding. (d) If F is bijective, it is a homeomorphism.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — proper

FC08-CA-U073 · Appendix A, § Connectedness and Compactness; source L18420 · not formalized

If X and Y are topological spaces, a map F X Y (continuous or not) is said to be proper if for every compact set K Y , the preimage F .K/ is compact. Here are some useful sufficient conditions for a map to be proper.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Proposition A.53

FC08-CA-U074 · Appendix A, § Connectedness and Compactness; source L18422 · not formalized

(Sufficient Conditions for Properness). Suppose $X$ and $Y$ are topological spaces and $F \colon X \to Y$ is continuous. (a) If $X$ is compact and $Y$ is Hausdorff, $F$ is proper. (b) If $F$ is a closed map with compact fibers, $F$ is proper. (c) If $F$ is a topological embedding with closed image, $F$ is proper. (d) If $Y$ is Hausdorff and $F$ has a continuous left inverse $G \colon Y \to X$ with $G \circ F = \operatorname{Id}_{X}$, then $F$ is proper. (e) If $F$ is proper and $A \subseteq X$ is saturated with respect to $F$, then $F|_{A} \colon A \to F(A)$ is proper.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — metrizable

FC08-CA-U075 · Appendix A, § Locally Compact Hausdorff Spaces; source L18438 · in Mathlib

In general, the topological spaces whose properties are most familiar are those whose topologies are induced by metrics; such a topological space is said to be metrizable. However, when studying manifolds, it is often quite inconvenient to exhibit a metric that generates a manifold’s topology. Fortunately, as shown in Chapter 1, manifolds belong to another class of spaces with similarly nice properties, the locally compact Hausdorff spaces. In this section, we review some of the properties of these spaces.

Formalized. Mathlib/Topology/Metrizable/Basic.lean::MetrizableSpace — MetrizableSpace is exactly existence of a metric inducing the given topology.

Definition/convention — locally compact

FC08-CA-U076 · Appendix A, § Locally Compact Hausdorff Spaces; source L18440 · in Mathlib

A topological space X is said to be locally compact if every point has a neighborhood contained in a compact subset of X. If X is Hausdorff, this property has two equivalent formulations that are often more useful, as the next exercise shows. A subset of X is said to be precompact in X if its closure in X is compact.

Formalized. Mathlib/Topology/Defs/Filter.lean::LocallyCompactSpace; Mathlib/Topology/Separation/Basic.lean::Bornology.relativelyCompact, Bornology.relativelyCompact.isBounded_iff — LocallyCompactSpace is the compact-neighborhood condition; the relatively-compact bornology identifies precompact sets exactly by compact closure.

Theorem A.57

FC08-CA-U077 · Appendix A, § Locally Compact Hausdorff Spaces; source L18454 · in Mathlib

Theorem A.57 (Proper Continuous Maps Are Closed). Suppose X is a topological space and Y is a locally compact Hausdorff space. Then every proper continuous map $F \colon X \to Y$ is clos f $T$ , so in fact $d ( \theta + \alpha ) = 0$ on all of U .

Formalized. Mathlib/Topology/Maps/Proper/CompactlyGenerated.lean::isProperMap_iff_isCompact_preimage; Mathlib/Topology/Maps/Proper/Basic.lean::IsProperMap.isClosedMap — For a locally compact Hausdorff target, the compact-preimage criterion is equivalent to Mathlib properness, whose isClosedMap theorem gives Lee’s conclusion.

Theorem A.58

FC08-CA-U078 · Appendix A, § Locally Compact Hausdorff Spaces; source L18460 · in Mathlib

Theorem A.58 (Baire Category Theorem). In a locally compact Hausdorff space or a complete metric space, every countable union of nowhere dense sets has empty interior. C

Formalized. Mathlib/Topology/Baire/CompleteMetrizable.lean::BaireSpace.of_completelyPseudoMetrizable; Mathlib/Topology/Baire/LocallyCompactRegular.lean::BaireSpace.of_t2Space_locallyCompactSpace — Mathlib supplies Baire-space instances for complete metrizable and locally compact Hausdorff spaces; its Baire-space axiom is equivalent to the source nowhere-dense-union formulation.

Corollary A.59

FC08-CA-U079 · Appendix A, § Locally Compact Hausdorff Spaces; source L18462 · not formalized

Corollary A.59. In a locally compact Hausdorff space or a complete metric space, every nonempty countable closed subset contains at least one isolated point.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — exhaustion of X by compact sets

FC08-CA-U080 · Appendix A, § Locally Compact Hausdorff Spaces; source L18466 · in Mathlib

If we add the hypothesis of second-countability to a locally compact Hausdorff space, we can prove even more. A sequence $( K _ { i } ) _ { i = 1 } ^ { \infty }$ of compact subsets of a topological space X is called an exhaustion of X by compact sets if $\textstyle X = \bigcup _ { i } K _ { i }$ and

Formalized. Mathlib/Topology/Compactness/SigmaCompact.lean::CompactExhaustion — CompactExhaustion has exactly Lee’s fields: compact K n, K n ⊆ interior (K (n+1)), and union equal to the whole space.

Proposition A.60

FC08-CA-U081 · Appendix A, § Locally Compact Hausdorff Spaces; source L18468 · in Mathlib

A second-countable, locally compact Hausdorff space admits an exhaustion by compact sets.

Formalized. Mathlib/Topology/Compactness/SigmaCompact.lean::sigmaCompactSpace_of_locallyCompact_secondCountable, CompactExhaustion.choice — Second-countable locally compact spaces are σ-compact, and CompactExhaustion.choice constructs exactly the exhaustion defined in U080.

Definition/convention — homotopic relative to A

FC08-CA-U082 · Appendix A, § Homotopy and the Fundamental Group; source L18474 · in Mathlib

If X and Y are topological spaces and $F _ { 0 } , F _ { 1 } \colon X Y$ are continuous maps, a homotopy from $\pmb { F _ { 0 } }$ to ${ \cal F } _ { 1 }$ is a continuous map $H \colon X \times I \to Y$ satisfying \[ \begin{array}{l} H (x, 0) = F _ {0} (x), \\ H (x, 1) = F _ {1} (x), \end{array} \] for all $x \in X$ . If there exists a homotopy from $F _ { 0 }$ to $F _ { 1 }$ , we say that $\pmb { F _ { 0 } }$ and ${ \cal F } _ { 1 }$ are homotopic, and write $F _ { 0 } \simeq F _ { 1 }$ . If the homotopy satisfies $H ( x , t ) = F _ { 0 } ( x ) = F _ { 1 } ( x )$ for all $t \in I$ and all x in some subset $A \subseteq X$ , the maps $F _ { 0 }$ and $F _ { 1 }$ are said to be homotopic relative to A. Both “homotopic” and “homotopic relative to $A ^ { \ast }$ are equivalence relations on the set of all continuous maps from $X$ to $Y$.

Formalized. Mathlib/Topology/Homotopy/Basic.lean::ContinuousMap.Homotopic, ContinuousMap.Homotopic.refl, ContinuousMap.Homotopic.symm, ContinuousMap.Homotopic.trans, ContinuousMap.HomotopicRel — Homotopic and HomotopicRel are the interval-homotopy and relative-homotopy relations; the displayed refl/symm/trans theorems prove the source equivalence-relation clause.

Definition/convention — path-homotopic

FC08-CA-U083 · Appendix A, § Homotopy and the Fundamental Group; source L18482 · in Mathlib

Two paths $f_{0}, f_{1} \colon I \to X$ are path-homotopic, written $f_{0} \sim f_{1}$, if they are homotopic relative to $\{0,1\}$; explicitly, there is a continuous map $H \colon I \times I \to X$ with \[ H(s,0) = f_{0}(s), \quad H(s,1) = f_{1}(s) \quad (s \in I), \qquad H(0,t) = f_{0}(0) = f_{1}(0), \quad H(1,t) = f_{0}(1) = f_{1}(1) \quad (t \in I). \] For fixed $p, q \in X$, path homotopy is an equivalence relation on the paths from $p$ to $q$; the class of $f$ is its path class $[f]$.

Formalized. Mathlib/Topology/Homotopy/Path.lean::Path.Homotopic — Path.Homotopic is homotopy relative to the two endpoints, exactly Lee’s path-homotopy relation.

Definition/convention — its path class

FC08-CA-U084 · Appendix A, § Homotopy and the Fundamental Group; source L18488 · in Mathlib

For any given points $p , q \in X$ , path homotopy is an equivalence relation on the set of all paths from $p$ to $q$ . The equivalence class of a path $f$ is called its path class, and is denoted by Œf .

Formalized. Mathlib/Topology/Homotopy/Path.lean::Path.Homotopic.Quotient — The quotient by path homotopy is exactly the set of path classes between fixed endpoints.

Definition/convention — fundamental group of X based at

FC08-CA-U085 · Appendix A, § Homotopy and the Fundamental Group; source L18498 · in Mathlib

If X is a topological space and $q$ is a point in X, a loop in X based at q is a path in X from $q$ to $q$ , that is, a continuous map $f \colon I \to X$ such that $f ( 0 ) = f ( 1 ) = q$ The set of path classes of loops based at q is denoted by $\pi _ { 1 } ( X , q )$ . Equipped with the product described above, it is a group, called the fundamental group of X based at $\pmb q$ . The identity element of this group is the path class of the constant path $c _ { q } ( s ) \equiv q$ , and the inverse of $[ f ]$ is the path class of the reverse path ${ \overline { { f } } } ( s ) =$ $f ( 1 - s )$ It can be shown that the fundamental groups at different base points of a path-connected space are isomorphic.

Formalized. Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup — FundamentalGroup X q is the automorphism group at q in the path-homotopy fundamental groupoid, i.e. path classes of based loops with concatenation, constant identity, and reversal inverse.

Definition/convention — source terminology/construction

FC08-CA-U086 · Appendix A, § Homotopy and the Fundamental Group; source L18500 · not formalized

$f ( 1 - s )$ It can be shown that for path-connected spaces, the fundamental groups based at different points are isomorphic. If X is path-connected and for some (hence every) $q \in X$ , the fundamental group $\pi _ { 1 } ( X , q )$ is the trivial group consisting of $[ c _ { q } ]$ alone, we say that X is simply connected. This means that every loop is path-homotopic to a constant path.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib/TauCeti contain substantial fundamental-group and homotopy infrastructure, but this row bundles basepoint transport, composition/functoriality clauses, sphere/product computations, or a concrete deformation example without one complete checked owner at the required interface. Strict whole-row semantics reject partial clause coverage and unbridged reconstruction.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Proposition A.62

FC08-CA-U087 · Appendix A, § Homotopy and the Fundamental Group; source L18506 · not formalized

$F _ { 0 } , F _ { 1 } \colon X Y$ and $G _ { 0 } , G _ { 1 } \colon Y \to Z$ are continuous maps with $F _ { 0 } \simeq F _ { 1 }$ and $G _ { 0 } \simeq G _ { 1 }$ , then $G _ { 0 } \circ F _ { 0 } \simeq G _ { 1 } \circ F _ { 1 }$ . Similarly, $i f f _ { 0 } , f _ { 1 } \colon I \to X$ are path-homotopic and $F \colon X \to Y$ is a contin the value of du along S for our eventual solution u.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Proposition A.64

FC08-CA-U088 · Appendix A, § Homotopy and the Fundamental Group; source L18516 · in Mathlib

Proposition A.64. If X and Y are topological spaces and $F \colon X \to Y$ is a continuous map, then $F _ { * } \colon \pi _ { 1 } ( X , q ) \to \pi _ { 1 } ( Y , F ( q ) )$ is a group homomorphism, known as the homomorphism induced by $F$.

Formalized. Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup.map — A continuous map induces exactly the stated group homomorphism on based fundamental groups.

Proposition A.65

FC08-CA-U089 · Appendix A, § Homotopy and the Fundamental Group; source L18518 · not formalized

Proposition A.65 (Properties of the Induced Homomorphism). (a) Let $F \colon X \to Y$ and $G \colon Y \to Z$ be continuous maps. Then for each $q \in X$ $( G \circ F ) _ { * } = G _ { * } \circ F _ { * } \colon \pi _ { 1 } ( X , q ) \to \pi _ { 1 } { \bigl ( } Z , G ( F ( q ) ) { \bigr ) }$ (b) For each space X and each $q \in X$ , the homomorphism induced by the identity map IdX $X X$ is the identity map of $\pi _ { 1 } ( X , q )$ (c) If $F \colon X \to Y$ is a homeomorphism, then $F _ { * } \colon \pi _ { 1 } ( X , q ) \to \pi _ { 1 } { \bigl ( } Y , F ( q ) { \bigr ) }$ is an isomorphism. Thus, homeomorphic spaces have isomorphic fundamental groups.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Proposition A.68

FC08-CA-U090 · Appendix A, § Homotopy and the Fundamental Group; source L18530 · not formalized

(Fundamental Groups of Spheres). (a) $\pi_{1}(\mathbb{S}^{1},(1,0))$ is the infinite cyclic group generated by the path class of the loop $\omega \colon I \to \mathbb{S}^{1}$ given by $\omega(s) = (\cos 2\pi s,\ \sin 2\pi s)$. (b) If $n > 1$, then $\mathbb{S}^{n}$ is simply connected.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Proposition A.69

FC08-CA-U091 · Appendix A, § Homotopy and the Fundamental Group; source L18536 · not formalized

Proposition A.69 (Fundamental Groups of Product Spaces). Suppose $X _ { 1 } , \ldots , X _ { k }$ are topological spaces, and let $p _ { i } \colon X _ { 1 } \times \cdots \times X _ { k } \to X _ { i }$ denote the ith projection map. For any points $q _ { i } \in X _ { i } , i = 1 , \dots , k$ , define a map \[ P \colon \pi_ {1} \bigl (X _ {1} \times \dots \times X _ {k}, (q _ {1}, \ldots , q _ {k}) \bigr) \to \pi_ {1} (X _ {1}, q _ {1}) \times \dots \times \pi_ {1} (X _ {k}, q _ {k}) \] b \[ P [ f ] = \left(p _ {1 *} [ f ], \dots , p _ {k *} [ f ]\right). \] Then P is an isomorphism.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — homotopy inverse for F

FC08-CA-U092 · Appendix A, § Homotopy and the Fundamental Group; source L18552 · not formalized

continuous map $F \colon X \to Y$ between topological spaces is said to be a homotopy equivalence if there is a continuous map $G \colon Y \to X$ such that $F \circ G \simeq \operatorname { I d } _ { Y }$ and $G \circ F \simeq \operatorname { I d } _ { X }$ . Such a map G is called a homotopy inverse for F . If there exists a homotopy equivalence between X and Y , the two spaces are said to be homotopy equivalent. For example, the inclusion map $\iota \colon \mathbb { S } ^ { n - 1 } \hookrightarrow \mathbb { R } ^ { n } \setminus \{ 0 \}$ is a homotopy equivalence with homotopy inverse $r ( x ) = x / | x |$ , because $r \circ \iota = \mathrm { I d } _ { \mathbb { S } ^ { n - 1 } }$ and $\iota \circ r$ is homotopic to the identity map of $\mathbb { R } ^ { n } \setminus \{ 0 \}$ via t

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Theorem A.71

FC08-CA-U093 · Appendix A, § Homotopy and the Fundamental Group; source L18554 · in Mathlib

(Homotopy Invariance). If $F \colon X \to Y$ is a homotopy equivalence, then for each $p \in X$ the map $F_{*} \colon \pi_{1}(X,p) \to \pi_{1}(Y,F(p))$ is an isomorphism.

Formalized. Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean::FundamentalGroupoidFunctor.equivOfHomotopyEquiv; Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup.map — The equivalence of fundamental groupoids induced by a homotopy equivalence restricts at each basepoint to the source induced fundamental-group isomorphism.

Definition/convention — covering map

FC08-CA-U094 · Appendix A, § Covering Maps; source L18560 · not formalized

Suppose $E$ and $X$ are topological spaces. A map $\pi \colon E \to X$ is a covering map if $E$ and $X$ are connected and locally path-connected, $\pi$ is surjective and continuous, and every $p \in X$ has a neighborhood $U$ that is evenly covered by $\pi$, meaning each component of $\pi^{-1}(U)$ is mapped homeomorphically onto $U$ by $\pi$. Then $X$ is the base of the covering and $E$ a covering space of $X$; for an evenly covered $U$, the components of $\pi^{-1}(U)$ are the sheets of the covering over $U$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has covering and lifting infrastructure and TauCeti has later universal-cover classification results, but Lee’s row uses an augmented covering-map convention or a locally-simply-connected/universal-cover statement whose full hypotheses and uniqueness conclusion are not owned by one compatible checked declaration without a nontrivial bridge. Strict whole-row semantics reject partial clause coverage and unbridged reconstruction.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — lift of F

FC08-CA-U095 · Appendix A, § Covering Maps; source L18576 · not formalized

$\pi \colon E \to X$ is a covering map and $F \colon B \to X$ is a continuous map, a lift of F is a continuous map $\widetilde { F } \colon B \to E$ such that $\pi \circ { \tilde { F } } = F$

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Proposition A.77

FC08-CA-U096 · Appendix A, § Covering Maps; source L18580 · in Mathlib

(Lifting Properties of Covering Maps). Suppose $\pi \colon E \to X$ is a covering map. (a) Unique lifting property: if $B$ is connected and $F \colon B \to X$ is continuous, any two lifts of $F$ agreeing at one point are identical. (b) Path lifting property: if $f \colon I \to X$ is a path and $e \in E$ satisfies $\pi(e) = f(0)$, there is a unique lift $\widetilde{f}_{e} \colon I \to E$ of $f$ with $\widetilde{f}_{e}(0) = e$. (c) Monodromy theorem: if $f, g \colon I \to X$ are path-homotopic and $\widetilde{f}_{e}, \widetilde{g}_{e}$ are their lifts starting at the same $e \in E$, then those lifts are path-homotopic and $\widetilde{f}_{e}(1) = \widetilde{g}_{e}(1)$.

Formalized. Mathlib/Topology/Covering/Basic.lean::IsCoveringMap.eq_of_comp_eq; Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.exists_path_lifts, IsCoveringMap.liftPath, IsCoveringMap.homotopicRel_liftPath — eq_of_comp_eq is unique lifting from one agreed point on a connected source; path lifting gives the unique lifted path, and homotopicRel_liftPath gives homotopic lifts and hence equal lifted endpoints.

Proposition A.78

FC08-CA-U097 · Appendix A, § Covering Maps; source L18588 · in Mathlib

and $\widetilde { g } _ { e }$ are path-homotopic and $\widetilde f _ { e } ( 1 ) = \widetilde g _ { e } ( 1 )$ Proposition A.78 (Lifting Criterion). Suppose $\pi \colon E \to X$ is a covering map, Y is a connected and locally path-connected space, and F $Y X$ is a continuous map. Let $y \in Y$ and $e \in E$ be such that $\pi ( e ) = F ( y )$ . Then there exists a lift $\widetilde { F } \colon Y \to \dot { E }$ of F satisfying $\widetilde F ( y ) = e$ if and only if $F _ { * } \left( \pi _ { 1 } ( Y , y ) \right) \subseteq \pi _ { * } { \bigl ( } \pi _ { 1 } ( E , e ) { \bigr ) }$ Proposition A.79 (Coverings

Formalized. Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le — This is the fundamental-group image containment criterion for existence and uniqueness of a lift with prescribed basepoint, exactly Lee’s lifting criterion.

Proposition A.79

FC08-CA-U098 · Appendix A, § Covering Maps; source L18590 · not formalized

(Coverings of Simply Connected Spaces). If $X$ is simply connected, then every covering map $\pi \colon E \to X$ is a homeomorphism.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — locally simply connected

FC08-CA-U099 · Appendix A, § Covering Maps; source L18592 · not formalized

A topological space is said to be locally simply connected if it admits a basis of simply connected open subsets.

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Proposition A.80

FC08-CA-U100 · Appendix A, § Covering Maps; source L18594 · not formalized

Proposition A.80 (Existence of a Universal Covering Space). If X is a connected and locally simply connected topological space, there exists a simply connected topological space $\widetilde { X }$ and a covering map ${ \tilde { X } } \to X . \ I f { \widehat { \pi } } \colon { \hat { X } } \to { \bar { X } }$ is any other simply connected covering of X, there is a homeomorphism $\varphi \colon { \tilde { X } } { \hat { X } }$ such that ${ \hat { \pi } } \circ \varphi = \pi$

Searched: N=2026-09-07; A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=5315eef9e4ffb98e0f89f278b765c50a149f66ca

Definition/convention — universal covering space of X

FC08-CA-U101 · Appendix A, § Covering Maps; source L18596 · in Mathlib

${ \hat { \pi } } \circ \varphi = \pi$ The simply connected covering space $\widetilde { X }$ whose existence and uniqueness (up to homeomorphism) are guaranteed by this proposition is called the universal covering space roblem, but they are not equal in any open subset.

Formalized. Mathlib/Topology/Covering/Basic.lean::IsCoveringMap; Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean::SimplyConnectedSpace — A universal covering space is exactly a covering map whose total space is simply connected; these two checked interfaces encode the source definition.