Commit 2024-11-14 05:52 8b6dfe34

View on Github →

feat(AlgebraicTopology/SimplicialSet): applications of the simplicial identities (#18743) For each of the generating simplicial identities, we provide a corresponding application lemma in simplicial sets.

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

modified theorem SimplexCategory.δ_comp_δ'

modified theorem SimplexCategory.δ_comp_δ_self'

modified theorem SimplexCategory.δ_comp_δ_self

modified theorem SimplexCategory.δ_comp_σ_of_gt

modified theorem SimplexCategory.δ_comp_σ_of_le

modified theorem SimplexCategory.δ_comp_σ_self'

modified theorem SimplexCategory.δ_comp_σ_succ'

Modified Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

added theorem SSet.δ_comp_δ''_apply

added theorem SSet.δ_comp_δ'_apply

added theorem SSet.δ_comp_δ_apply

added theorem SSet.δ_comp_δ_self'_apply

added theorem SSet.δ_comp_δ_self_apply

added theorem SSet.δ_comp_σ_of_gt'_apply

added theorem SSet.δ_comp_σ_of_gt_apply

added theorem SSet.δ_comp_σ_of_le_apply

added theorem SSet.δ_comp_σ_self'_apply

added theorem SSet.δ_comp_σ_self_apply

added theorem SSet.δ_comp_σ_succ'_apply

added theorem SSet.δ_comp_σ_succ_apply

added theorem SSet.σ_comp_σ_apply