Commit 2024-01-10 21:36 7cade347

View on Github →

feat(AlgebraicTopology/Quasicategory): alternative statement of hornfilling condition (#9360)

Estimated changes

Modified Mathlib/AlgebraicTopology/Quasicategory.lean

added theorem SSet.quasicategory_of_filler

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

added def SimplexCategory.factor_δ

added theorem SimplexCategory.factor_δ_spec

Modified Mathlib/AlgebraicTopology/SimplicialObject.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet.lean

added def SSet.horn.face

added theorem SSet.horn.hom_ext