Commit 2025-02-07 17:49 0a9e4e43

View on Github →

feat(AlgebraicTopology): instances on the topological simplices (#21555) which allows us to calculate the singular simplicial set of a totally disconnected space.

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

Modified Mathlib/AlgebraicTopology/SingularSet.lean

added def TopCat.toSSetIsoConst

Modified Mathlib/AlgebraicTopology/TopologicalSimplex.lean

added def SimplexCategory.toTopObjOneHomeo

added theorem SimplexCategory.toTopObj_one_add_eq_one

added theorem SimplexCategory.toTopObj_one_coe_add_coe_eq_one

added theorem SimplexCategory.toTopObj_zero_apply_zero

Modified Mathlib/Topology/Connected/TotallyDisconnected.lean

added theorem TotallyDisconnectedSpace.eq_of_continuous

Modified Mathlib/Topology/UnitInterval.lean

added theorem unitInterval.coe_toNNReal

added def unitInterval.toNNReal

added theorem unitInterval.toNNReal_continuous