@[reducible, inline]

abbrev CWComplex (X : Type u_1) [TopologicalSpace X] : Type (u_1 + 1)

A CW-complex structure on a topological space X, identified with a CW-complex structure on the universe set Set.univ : Set X from mathlib's Topology.CWComplex.

@[reducible, inline]

abbrev CWComplex.cells (X : Type u_2) [TopologicalSpace X] [Topology.CWComplex Set.univ] (n : ℕ) : Type u_2

The indexing type of n-cells in a CW-complex X. These are the cells $A_n$ appearing in the attaching pushout for $\mathrm{Sk}_n X$.

@[reducible, inline]

noncomputable abbrev CWComplex.skeleton (X : Type u_2) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ∞) : Topology.RelCWComplex.Subcomplex Set.univ

The n-skeleton $\mathrm{Sk}_n X$ of a CW-complex, defined for n : ℕ∞. This is the subspace obtained by attaching all cells of dimension at most n, as in Definition 14.5.

def CWComplex.IsFiniteDimensional (X : Type u_2) [TopologicalSpace X] [Topology.CWComplex Set.univ] : Prop

A CW-complex is finite-dimensional (Definition 14.7) if there is some n beyond which there are no cells, i.e., $\mathrm{Sk}_n X = X$ for some n.

def CWComplex.IsFiniteType (X : Type u_2) [TopologicalSpace X] [Topology.CWComplex Set.univ] : Prop

A CW-complex is of finite type (Definition 14.7) if each set of n-cells $A_n$ is finite.

def CWComplex.IsFinite (X : Type u_2) [TopologicalSpace X] [Topology.CWComplex Set.univ] : Prop

A CW-complex is finite (Definition 14.7) if it is both finite-dimensional and of finite type. Equivalently, it has only finitely many cells in total.

structure CWComplex.CWComplexProperties : Type (max (max (u_4 + 1) (u_5 + 1)) (u_6 + 1))

A bundle of the three properties of CW-complexes stated in Theorem 14.8: every CW-complex is Hausdorff, compactness is equivalent to finiteness, and every compact smooth manifold admits a CW-structure.

• hausdorff (X : Type u_2) [TopologicalSpace X] [Topology.CWComplex Set.univ] : T2Space X
• compact_iff_finite (X : Type u_3) [TopologicalSpace X] [Topology.CWComplex Set.univ] : CompactSpace X ↔ IsFinite X
• manifold_admits_cw {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ⊤ M] [CompactSpace M] : Topology.CWComplex Set.univ

theorem CWComplex.cwComplex_t2Space (X : Type u_2) [TopologicalSpace X] [Topology.CWComplex Set.univ] : T2Space X

Theorem 14.8 (first part): every CW-complex is Hausdorff.

theorem CWComplex.cwComplex_compactSpace_iff_isFinite (X : Type u_2) [TopologicalSpace X] [Topology.CWComplex Set.univ] : CompactSpace X ↔ IsFinite X

Theorem 14.8 (second part): a CW-complex is compact if and only if it is finite.

noncomputable def CWComplex.compact_smooth_manifold_admits_cwStructure {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ⊤ M] [CompactSpace M] : Topology.CWComplex Set.univ

Theorem 14.8 (third part): every compact smooth manifold admits a CW-structure.

noncomputable def CWComplex.cwComplexProperties : CWComplexProperties

Packaging Theorem 14.8 into the CWComplexProperties structure, combining the Hausdorff property, the compactness/finiteness equivalence, and CW-structures on compact smooth manifolds.