Commit 2025-11-14 17:31 c4848a19

View on Github →

feat(AlgebraicTopology): Edge and CompStruct for simplicial sets (#31265) The API for 2-truncated simplicial sets #31254 is reproduced for simplicial sets. The definitions for simplicial sets are defeq to their 2-truncated counterparts, but an effort is made to contain abuse of defeq...

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialSet/CompStruct.lean

added def SSet.Edge.CompStruct.compId

added theorem SSet.Edge.CompStruct.compId_simplex

added theorem SSet.Edge.CompStruct.exists_of_simplex

added theorem SSet.Edge.CompStruct.ext

added def SSet.Edge.CompStruct.idComp

added theorem SSet.Edge.CompStruct.idComp_simplex

added def SSet.Edge.CompStruct.map

added theorem SSet.Edge.CompStruct.map_simplex

added def SSet.Edge.CompStruct.mk

added theorem SSet.Edge.CompStruct.mk_simplex

added def SSet.Edge.CompStruct.ofTruncated

added def SSet.Edge.CompStruct.simplex

added def SSet.Edge.CompStruct.toTruncated

added def SSet.Edge.CompStruct

added def SSet.Edge.edge

added theorem SSet.Edge.exists_of_simplex

added theorem SSet.Edge.ext

added def SSet.Edge.id

added theorem SSet.Edge.id_edge

added def SSet.Edge.map

added theorem SSet.Edge.map_id

added def SSet.Edge.mk'

added theorem SSet.Edge.mk'_edge

added def SSet.Edge.ofTruncated

added theorem SSet.Edge.ofTruncated_edge

added theorem SSet.Edge.src_eq

added theorem SSet.Edge.tgt_eq

added def SSet.Edge.toTruncated

added theorem SSet.Edge.toTruncated_edge

added def SSet.Edge

Modified Mathlib/AlgebraicTopology/SimplicialSet/CompStructTruncated.lean