Commit 2026-04-11 09:33 0410bdeb

View on Github →

feat(AlgebraicTopology/SimplicialSet): more API for the boundary (#37692)

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean

added theorem SSet.boundary_lt_top

added theorem SSet.boundary_obj_eq_univ

added theorem SSet.face_singleton_compl_le_boundary

added theorem SSet.stdSimplex.le_boundary_iff

added theorem SSet.stdSimplex.notMem_boundary

added theorem SSet.stdSimplex.subcomplex_hasDimensionLT_of_neq_top

Modified Mathlib/AlgebraicTopology/SimplicialSet/Dimension.lean

deleted theorem SSet.degenerate_eq_top_of_hasDimensionLT

added theorem SSet.degenerate_eq_univ_of_hasDimensionLT

deleted theorem SSet.nonDegenerate_eq_bot_of_hasDimensionLT

added theorem SSet.nonDegenerate_eq_empty_of_hasDimensionLT

Modified Mathlib/AlgebraicTopology/SimplicialSet/Finite.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/KanComplex/MulStruct.lean

added def SSet.PtSimplex.RelStruct.copy

added def SSet.PtSimplex.RelStruct.ofEq

added def SSet.PtSimplex.RelStruct.refl

added theorem SSet.PtSimplex.comp_map_eq_const

added theorem SSet.PtSimplex.δ_map

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

added theorem SSet.stdSimplex.map_objEquiv_symm

added theorem SSet.stdSimplex.nonDegenerate_top_dim

added theorem SSet.stdSimplex.not_hasDimensionLT

added theorem SSet.stdSimplex.objEquiv_symm_id_mem_nonDegenerate

added theorem SSet.stdSimplex.ofSimplex_objEquiv_symm_id