Structures · Topology

Topology.RelCWComplex

A CW complex of a topological space X relative to another subspace D is the data of its `n`-cells cell n i for each n : ℕ along with attaching maps that satisfy a number of properties with the most important being closure-finiteness (mapsTo) and weak topology (closed'). Note that this definition requires C and D to be closed subspaces. If C is not closed choose X to be C.

Defined in

Mathlib.Topology.CWComplex.Classical.Basic

Shape

2 explicit arguments · adds cell, map, source_eq, continuousOn, continuousOn_symm, pairwiseDisjoint', disjointBase', mapsTo, closed', isClosedBase, union'