FC07 — Hatcher, Algebraic Topology
This book contains 137 definitions, 71 theorems, 116 propositions, 27 lemmas, 47 corollaries, 152 examples, 54 constructions, 5 conventions and 3 other statements.
612 of its 612 statements have been checked against Lean; 102 of those are formalized somewhere.
| Chapter | Definitions | Theorems, propositions | Lemmas, corollaries | Everything else | Formalized | Not formalized |
|---|---|---|---|---|---|---|
| Chapter 0. Some Underlying Geometric Notions | 10 | 4 | 2 | 25 | 11 | 30 |
| Chapter 1. The Fundamental Group | 21 | 30 | 7 | 36 | 44 | 50 |
| Chapter 2. Homology | 25 | 29 | 11 | 33 | 20 | 78 |
| Chapter 3. Cohomology | 34 | 42 | 19 | 64 | 12 | 147 |
| Chapter 4. Homotopy Theory | 38 | 67 | 31 | 52 | 5 | 183 |
| Appendix. Topology of Cell Complexes | 9 | 15 | 4 | 4 | 10 | 22 |
What the book contains
| Kind of statement | Count |
|---|---|
| Definitions | 137 |
| Theorems | 71 |
| Propositions | 116 |
| Lemmas | 27 |
| Corollaries | 47 |
| Examples | 152 |
| Constructions | 54 |
| Conventions | 5 |
| Other statements | 3 |
| Total | 612 |
Where its statements stand in Lean
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 510 | 83% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 82 | 13% | Mathlib states and proves it. |
| in another Lean project | 20 | 3% | Some other Lean development has it; using it means porting that code. |
| checked in total | 612 |
How this book was read
Corpus source: FC07 in Foundational source corpus v1 (frozen).
This is the canonical Sweep-I source-unit catalogue for FC07. Stable source-local IDs are consumed unchanged by Sweeps II–IV.
Frozen source: Hatcher - 2002 - Algebraic Topology.md
Scope: complete book, Chapters 0–4 and Appendix; exercises excluded item-by-item. Stable IDs are chapter-local and source-ordered; dependencies point only to strictly earlier FC07 units.