Commit 2026-06-24 10:56 c54f3c8d

View on Github →

feat(Topology/CWComplex/Classical): discrete spaces are CW complexes (#38943) as well as some useful lemmas This is partly based on code by @scholzhannah I think this is notable to include, since it is pretty much the only (easy) "topological" sufficient condition for something being a CW complex there is.

Estimated changes

Modified Mathlib/Algebra/Group/Fin/Tuple.lean

added theorem Matrix.finZeroElim_eq_zero

Modified Mathlib/Topology/CWComplex/Classical/Basic.lean

added def Topology.CWComplex.OfDiscreteClosed

added theorem Topology.RelCWComplex.closedCell_nonempty

added theorem Topology.RelCWComplex.openCell_congr

added theorem Topology.RelCWComplex.openCell_nonempty

Modified Mathlib/Topology/Covering/Basic.lean

Modified Mathlib/Topology/DiscreteSubset.lean

added theorem isClosed_of_subset_discrete_closed

deleted theorem isDiscrete_iff_forall_exists_isOpen

added theorem isDiscrete_iff_forall_mem_exists_isClosed

added theorem isDiscrete_iff_forall_mem_exists_isOpen

added theorem isDiscrete_iff_forall_subset_exists_isOpen

Modified Mathlib/Topology/Irreducible.lean