Commit 2025-06-17 04:30 e6c1288b

View on Github →

feat(Topology/CWComplex/Classical/Basic.lean): basic lemmas about CW complexes (#25973)

Estimated changes

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

added theorem Topology.CWComplex.eq_of_eq_union_iUnion

added theorem Topology.RelCWComplex.eq_of_eq_union_iUnion

added theorem Topology.RelCWComplex.iUnion_skeletonLT_eq_complex

added theorem Topology.RelCWComplex.iUnion_skeleton_eq_complex