Mathlib v3 is deprecated. Go to Mathlib v4

Theorem simplex_category.eq_σ_comp_of_not_injective

Modification history

2022-03-03 17:48
src/algebraic_topology/simplex_category.lean
feat(simplex_category): various epi/mono lemmas (#11924)
Added simplex_category.eq_σ_comp_of_not_injectiveView on Github →