CW complexes are delta-generated, hence locally path-connected

A Hausdorff relative CW complex C with base D is a quotient of the disjoint union of D and of one closed unit ball of Fin n → ℝ for each n-cell (TauCeti.isQuotientMap_sumElim_base_map). Closed balls of Fin n → ℝ are delta-generated (TauCeti.instDeltaGeneratedSpaceClosedBall), and disjoint unions and quotients of delta-generated spaces are delta-generated. So C is delta-generated as soon as its base is (TauCeti.deltaGeneratedSpace_of_relCWComplex), and every Hausdorff CW complex is delta-generated (TauCeti.instDeltaGeneratedSpaceCWComplex, and TauCeti.instDeltaGeneratedSpaceOfCWComplexUniv for a CW structure on the whole space).

Delta-generated spaces are locally path-connected and sequential (Mathlib's instances for DeltaGeneratedSpace), so with these instances every Hausdorff CW complex is a LocallyPathConnectedSpace and a SequentialSpace. Local path-connectedness is one of the standing hypotheses of covering-space theory: a path-connected, locally path-connected and semilocally simply connected space has a universal cover.

Main results

• TauCeti.deltaGeneratedSpace_of_relCWComplex: a Hausdorff relative CW complex over a delta-generated base is delta-generated.
• TauCeti.instDeltaGeneratedSpaceCWComplex: a Hausdorff CW complex is delta-generated.
• TauCeti.instDeltaGeneratedSpaceOfCWComplexUniv: a Hausdorff space with a CW structure on the whole space is delta-generated.

References

• A. Hatcher, Algebraic Topology, Appendix, Proposition A.4: CW complexes are locally contractible, in particular locally path-connected.

theorem TauCeti.deltaGeneratedSpace_of_relCWComplex {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] [DeltaGeneratedSpace ↑D] : DeltaGeneratedSpace ↑C

A relative CW complex over a delta-generated base is delta-generated. For example, this applies to a CW complex, whose base is empty.

instance TauCeti.instDeltaGeneratedSpaceCWComplex {X : Type u} [TopologicalSpace X] [T2Space X] {C : Set X} [Topology.CWComplex C] : DeltaGeneratedSpace ↑C

A Hausdorff CW complex is delta-generated, so in particular locally path-connected.

instance TauCeti.instDeltaGeneratedSpaceOfCWComplexUniv {X : Type u} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] : DeltaGeneratedSpace X

A Hausdorff space with a CW structure on the whole space is delta-generated, so in particular locally path-connected.