Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-03 17:48 5159a8fb

View on Github →

feat(simplex_category): various epi/mono lemmas (#11924)

Estimated changes

Modified src/algebraic_topology/simplex_category.lean

added theorem simplex_category.eq_comp_δ_of_not_surjective'

added theorem simplex_category.eq_comp_δ_of_not_surjective

added theorem simplex_category.eq_id_of_epi

added theorem simplex_category.eq_id_of_is_iso

added theorem simplex_category.eq_id_of_mono

added theorem simplex_category.eq_δ_of_mono

added theorem simplex_category.eq_σ_comp_of_not_injective'

added theorem simplex_category.eq_σ_comp_of_not_injective

added theorem simplex_category.eq_σ_of_epi

added theorem simplex_category.is_iso_of_bijective

added theorem simplex_category.iso_eq_iso_refl

added def simplex_category.order_iso_of_iso

Modified src/data/fin/basic.lean

added theorem fin.cast_succ_lt_iff_succ_le