Commit 2024-09-29 14:59 e060e71a

feat(Topology): define (relative) CW-complexes (#12502) We define a relative CW-complex as the colimit of an expanding sequence of subspaces sk i (called the $(i-1)$-skeleton) for i ≥ 0, where sk 0 (i.e., the $(-1)$-skeleton) is an arbitrary topological space, and each sk (n + 1) (i.e., the $n$-skeleton) is obtained from sk n (i.e., the $(n-1)$-skeleton) by attaching n-disks. This is based on David Wärn's suggestion on Zulip and Chapter 10 of A Concise Course in Algebraic Topology by J. P. May.