Commit 2023-04-06 10:57 56944fb6

View on Github →

feat: port AlgebraicTopology.SimplexCategory (#3286)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplexCategory.lean

added def SimplexCategory.Hom.comp

added theorem SimplexCategory.Hom.ext'

added theorem SimplexCategory.Hom.ext

added def SimplexCategory.Hom.id

added def SimplexCategory.Hom.mk

added theorem SimplexCategory.Hom.mk_toOrderHom

added theorem SimplexCategory.Hom.mk_toOrderHom_apply

added def SimplexCategory.Hom.toOrderHom

added theorem SimplexCategory.Hom.toOrderHom_mk

added def SimplexCategory.Truncated.inclusion

added def SimplexCategory.Truncated

added def SimplexCategory.const

added theorem SimplexCategory.const_comp

added theorem SimplexCategory.epi_iff_surjective

added theorem SimplexCategory.eq_comp_δ_of_not_surjective'

added theorem SimplexCategory.eq_comp_δ_of_not_surjective

added theorem SimplexCategory.eq_id_of_epi

added theorem SimplexCategory.eq_id_of_isIso

added theorem SimplexCategory.eq_id_of_mono

added theorem SimplexCategory.eq_δ_of_mono

added theorem SimplexCategory.eq_σ_comp_of_not_injective'

added theorem SimplexCategory.eq_σ_comp_of_not_injective

added theorem SimplexCategory.eq_σ_of_epi

added theorem SimplexCategory.ext

added theorem SimplexCategory.factorThruImage_eq

added theorem SimplexCategory.hom_zero_zero

added theorem SimplexCategory.image_eq

added theorem SimplexCategory.image_ι_eq

added theorem SimplexCategory.isIso_of_bijective

added theorem SimplexCategory.iso_eq_iso_refl

added theorem SimplexCategory.le_of_epi

added theorem SimplexCategory.le_of_mono

added def SimplexCategory.len

added theorem SimplexCategory.len_le_of_epi

added theorem SimplexCategory.len_le_of_mono

added theorem SimplexCategory.len_lt_of_mono

added theorem SimplexCategory.len_mk

added def SimplexCategory.mk

added def SimplexCategory.mkHom

added theorem SimplexCategory.mk_len

added theorem SimplexCategory.mono_iff_injective

added def SimplexCategory.orderIsoOfIso

added theorem SimplexCategory.skeletal

added theorem SimplexCategory.skeletalFunctor.coe_map

added def SimplexCategory.skeletalFunctor

added def SimplexCategory.toCat

added def SimplexCategory.δ

added theorem SimplexCategory.δ_comp_δ''

added theorem SimplexCategory.δ_comp_δ'

added theorem SimplexCategory.δ_comp_δ

added theorem SimplexCategory.δ_comp_δ_self'

added theorem SimplexCategory.δ_comp_δ_self

added theorem SimplexCategory.δ_comp_σ_of_gt'

added theorem SimplexCategory.δ_comp_σ_of_gt

added theorem SimplexCategory.δ_comp_σ_of_le

added theorem SimplexCategory.δ_comp_σ_self'

added theorem SimplexCategory.δ_comp_σ_self

added theorem SimplexCategory.δ_comp_σ_succ'

added theorem SimplexCategory.δ_comp_σ_succ

added def SimplexCategory.σ

added theorem SimplexCategory.σ_comp_σ

added def SimplexCategory

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.dite_val

added theorem Fin.ite_val