mathlib3

c965e54c - feat(algebraic_topology): the Čech nerve of a split epi has an extra degeneracy (#16779)

feat(algebraic_topology): the Čech nerve of a split epi has an extra degeneracy (#16779) In this PR, it is shown that the Čech nerve of a split epimorphism has an extra degeneracy. It is also shown that if two augmented simplicial objects are isomorphic, then an extra degeneracy for one of these transports as an extra degeneracy for the other.