Revision #3554 → #4084 · back to history
0935d082f4a5| Field | From #3554 | To #4084 |
|---|---|---|
| note | Mathlib has a classical `RelCWComplex`/`CWComplex` definition covering the notion referenced here. | The classical CW-complex classes `RelCWComplex`/`CWComplex` are defined in `Mathlib.Topology.CWComplex.Classical.Basic`. |
6d1bd4a67b154f5e6c034d35441dbcdb22ccecf91533dc410072f730fbc7f2fc48b9029a