Commit 2025-05-12 13:44 be7d03ad

View on Github →

feat: define singular manifolds (#15906) These are used to define bordism groups: the nth bordism group of a topological space X is the space of cobordism classes of all singular manifolds on X.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/Bordism.lean

added theorem SingularManifold.comap_M

added theorem SingularManifold.comap_f

added def SingularManifold.empty.{u}

added theorem SingularManifold.empty_M

added def SingularManifold.map.{u}

added theorem SingularManifold.map_M

added theorem SingularManifold.map_comp

added theorem SingularManifold.map_f

added def SingularManifold.prod

added def SingularManifold.sum

added theorem SingularManifold.sum_M

added theorem SingularManifold.sum_f

added def SingularManifold.toPUnit

added structure SingularManifold.{u}