Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-05 19:36 7ec52a1c

View on Github →

chore(algebraic_topology/simplex_category): removed ulift (#13183)

Estimated changes

Modified src/algebraic_topology/alternating_face_map_complex.lean

modified theorem algebraic_topology.map_alternating_face_map_complex

Modified src/algebraic_topology/simplex_category.lean

modified def simplex_category.const

modified theorem simplex_category.const_comp

modified theorem simplex_category.epi_iff_surjective

modified theorem simplex_category.eq_id_of_epi

modified theorem simplex_category.eq_id_of_is_iso

modified theorem simplex_category.eq_id_of_mono

modified theorem simplex_category.ext

modified def simplex_category.hom.comp

modified theorem simplex_category.hom.ext

modified def simplex_category.hom.id

modified def simplex_category.hom.mk

modified theorem simplex_category.hom.mk_to_order_hom

modified theorem simplex_category.hom.mk_to_order_hom_apply

modified def simplex_category.hom.to_order_hom

modified theorem simplex_category.hom.to_order_hom_mk

modified theorem simplex_category.is_iso_of_bijective

modified def simplex_category.is_skeleton_of

modified theorem simplex_category.iso_eq_iso_refl

modified def simplex_category.len

modified theorem simplex_category.len_le_of_epi

modified theorem simplex_category.len_le_of_mono

modified def simplex_category.mk

modified theorem simplex_category.mk_len

modified theorem simplex_category.mono_iff_injective

modified def simplex_category.order_iso_of_iso

modified theorem simplex_category.skeletal

modified def simplex_category.skeletal_functor

modified def simplex_category.truncated.inclusion

modified def simplex_category.truncated

modified def simplex_category

Modified src/algebraic_topology/simplicial_object.lean

modified def category_theory.cosimplicial_object.augmented.whiskering

modified def category_theory.cosimplicial_object.augmented.whiskering_obj

modified def category_theory.cosimplicial_object.truncated.whiskering

modified def category_theory.cosimplicial_object.truncated

modified def category_theory.cosimplicial_object.whiskering

modified def category_theory.cosimplicial_object

modified def category_theory.simplicial_object.augmented.whiskering

modified def category_theory.simplicial_object.augmented.whiskering_obj

modified def category_theory.simplicial_object.truncated.whiskering

modified def category_theory.simplicial_object.truncated

modified def category_theory.simplicial_object.whiskering

modified def category_theory.simplicial_object