Commit 2025-08-26 12:07 ca67c120

View on Github →

feat(AlgebraicToplogy/SimplexCategory): add notation for faces and degeneracies general truncated simplex categories (#26738)

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplexCategory/Truncated.lean

added theorem SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero

added theorem SimplexCategory.Truncated.δ₂_two_comp_σ₂_one

added theorem SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero

added theorem SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one

added theorem SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero

Modified Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

deleted theorem SSet.δ₂_one_comp_σ₂_zero

deleted theorem SSet.δ₂_two_comp_σ₂_one

deleted theorem SSet.δ₂_two_comp_σ₂_zero

deleted theorem SSet.δ₂_zero_comp_σ₂_one

deleted theorem SSet.δ₂_zero_comp_σ₂_zero