FC08 — Lee, Introduction to Smooth Manifolds

This book contains 509 definitions, 173 theorems, 287 propositions, 71 lemmas, 80 corollaries, 167 examples, 34 constructions, 79 conventions and 5 other statements.

1,405 of its 1,405 statements have been checked against Lean; 323 of those are formalized somewhere.

Chapter Definitions Theorems, propositions Lemmas, corollaries Everything else Formalized Not formalized
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 18 12 3 28 18 43
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 16 12 5 2 22 13
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 23 14 6 14 17 40
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 10 19 3 9 4 37
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 25 30 6 9 0 70
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 8 20 14 2 3 41
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 16 16 2 17 10 41
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 20 21 10 18 6 63
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 30 27 10 14 2 79
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 20 8 9 18 18 37
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 19 23 4 22 9 59
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 16 14 6 13 10 39
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 18 8 4 17 3 44
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 13 13 7 12 10 35
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 20 22 3 11 5 51
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 26 26 6 8 1 65
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 19 21 14 2 9 47
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 13 8 4 — 6 19
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 12 16 6 3 0 37
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 7 17 5 5 2 32
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 6 21 4 11 7 35
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 26 23 2 13 0 64
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 55 28 5 13 54 47
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 50 15 5 20 81 9
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 19 20 8 3 23 27
FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013) 4 6 — 1 3 8

What the book contains

Kind of statement Count
Definitions 509
Theorems 173
Propositions 287
Lemmas 71
Corollaries 80
Examples 167
Constructions 34
Conventions 79
Other statements 5
Total 1,405

Where its statements stand in Lean

Status Statements Share What it means
not formalized 1082 77% A documented search found no Lean statement of it anywhere.
in Mathlib 323 23% Mathlib states and proves it.
checked in total 1405

How this book was read

Corpus source: FC08 in Foundational source corpus v1 (frozen).

This is the canonical Sweep-I source-unit catalogue for FC08. Stable source-local IDs are consumed unchanged by Sweeps II–IV.

Frozen source: local-write-api-1783416009444-PW4NSUST_extracted.md.

Scope: complete book, Chapters 1–22 and Appendices A–D; inline Exercises and chapter-end Problems excluded item-by-item. Stable IDs are chapter-local and source-ordered; dependencies point only to strictly earlier FC08 units.

Inventory policy: definitions, constructions, conventions/notation, labeled theorems/propositions/corollaries/lemmas, and reusable labeled examples/comparisons. Exposition/history, proof-local temporary definitions, and later recaps are excluded as separate units.

Unit count: 1405 (778 labeled formal/example units; 627 definition/construction/convention/comparison units).