Commit 2025-03-11 09:14 4f7fb555

View on Github →

feat(AlgebraicTopology/SimplicialSet): degenerate simplices (#21098) This PR introduces the very basic definitions of degenerate and non degenerate simplices.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean

added def SSet.degenerate

added theorem SSet.degenerate_eq_iUnion_range_σ

added theorem SSet.degenerate_zero

added theorem SSet.exists_nonDegenerate

added theorem SSet.isIso_of_nonDegenerate

added theorem SSet.mem_degenerate_iff

added theorem SSet.mem_degenerate_iff_not_mem_nonDegenerate

added theorem SSet.mem_nonDegenerate_iff_not_mem_degenerate

added def SSet.nonDegenerate

added theorem SSet.nondegenerate_zero

added theorem SSet.σ_mem_degenerate