Def Topology.CWComplex.OfDiscreteClosed

Modification history

2026-06-24 10:56

Mathlib/Topology/CWComplex/Classical/Basic.lean

feat(Topology/CWComplex/Classical): discrete spaces are CW complexes (#38943) …

Added Topology.CWComplex.OfDiscreteClosed View on Github →