Commit 2023-04-29 23:07 18391382

View on Github →

feat: port AlgebraicTopology.ExtraDegeneracy (#3729)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

added theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base

added theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0

added theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ

added def SSet.Augmented.StandardSimplex.shift

added def SSet.Augmented.StandardSimplex.shiftFun

added theorem SSet.Augmented.StandardSimplex.shiftFun_0

added theorem SSet.Augmented.StandardSimplex.shiftFun_succ

added def SimplicialObject.Augmented.ExtraDegeneracy.map

added def SimplicialObject.Augmented.ExtraDegeneracy.ofIso

added structure SimplicialObject.Augmented.ExtraDegeneracy