Commit 2025-02-07 22:35 53d1998f

View on Github →

feat(AlgebraicTopology): notation ⦋n⦌ for SimplexCategory.mk n (#21565) We change the notation for SimplexCategory.mk n from [n] (which conflicts with the List notation) to ⦋n⦌. This also allows removing many type annotations of the form (⦋n⦌ : SimplexCategory). This was done in commit ceb03e9. Zulip poll

Estimated changes

modified theorem SimplexCategory.const_eq_id
modified def SimplexCategory.diag
modified theorem SimplexCategory.le_of_epi
modified theorem SimplexCategory.le_of_mono
modified theorem SimplexCategory.len_mk
modified def SimplexCategory.mkHom
modified theorem SimplexCategory.mk_len
modified def SimplexCategory.δ
modified def SimplexCategory.σ
modified def SSet.Truncated.δ0₂
modified def SSet.Truncated.δ1₂
modified def SSet.Truncated.δ2₂
modified def SSet.Truncated.ι0₂
modified def SSet.Truncated.ι1₂
modified def SSet.Truncated.ι2₂
modified theorem SSet.spine_map_vertex
modified def SSet.stdSimplex.id