Commit 2025-01-23 17:36 d6544fee

View on Github →

feat(AlgebraicTopology): rename standardSimplex to stdSimplex (#20974) Moves:

SSet.standardSimplex -> SSet.stdSimplex
SSet.standardSimplex.* -> SSet.stdSimplex.*

Estimated changes

Modified Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

Modified Mathlib/AlgebraicTopology/Quasicategory/StrictSegal.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

deleted theorem SSet.standardSimplex.coe_edge_down_toOrderHom

deleted theorem SSet.standardSimplex.coe_triangle_down_toOrderHom

deleted def SSet.standardSimplex.const

deleted theorem SSet.standardSimplex.const_down_toOrderHom

deleted def SSet.standardSimplex.edge

deleted def SSet.standardSimplex.id

deleted theorem SSet.standardSimplex.id_eq_objEquiv_symm

deleted theorem SSet.standardSimplex.map_apply

deleted theorem SSet.standardSimplex.map_id

deleted def SSet.standardSimplex.objEquiv

deleted theorem SSet.standardSimplex.objEquiv_id

deleted def SSet.standardSimplex.triangle

deleted def SSet.standardSimplex

added theorem SSet.stdSimplex.coe_edge_down_toOrderHom

added theorem SSet.stdSimplex.coe_triangle_down_toOrderHom

added def SSet.stdSimplex.const

added theorem SSet.stdSimplex.const_down_toOrderHom

added def SSet.stdSimplex.edge

added def SSet.stdSimplex.id

added theorem SSet.stdSimplex.id_eq_objEquiv_symm

added theorem SSet.stdSimplex.map_apply

added theorem SSet.stdSimplex.map_id

added def SSet.stdSimplex.objEquiv

added theorem SSet.stdSimplex.objEquiv_id

added def SSet.stdSimplex.triangle

added def SSet.stdSimplex

Modified Mathlib/AlgebraicTopology/SimplicialSet/Path.lean

deleted def SSet.standardSimplex.spineId

added def SSet.stdSimplex.spineId