Commit 2023-04-17 08:52 d286a1f7

View on Github →

feat: port AlgebraicTopology.TopologicalSimplex (#3437)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/TopologicalSimplex.lean

added theorem SimplexCategory.coe_toTopMap

added theorem SimplexCategory.continuous_toTopMap

added def SimplexCategory.toTop

added def SimplexCategory.toTopMap

added theorem SimplexCategory.toTopObj.ext

added def SimplexCategory.toTopObj

Modified Mathlib/Topology/Category/Top/Basic.lean

added theorem TopCat.hom_apply

modified theorem TopCat.id_app