Theorem CategoryTheory.Nerve.δ₀_eq

Modification history

2025-02-26 16:56
Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean
feat(AlgebraicTopology/NerveAdjunction): nerve adjunction infrastructure (#21885) …
Deleted CategoryTheory.Nerve.δ₀_eqView on Github →
2025-02-08 20:13
Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean
feat(AlgebraicTopology): notations X _⦋n⦌ and X ^⦋n⦌ for (co)simplicial objects (#21581) …
Modified CategoryTheory.Nerve.δ₀_eqView on Github →
2023-11-03 20:42
Mathlib/AlgebraicTopology/Nerve.lean
feat(CategoryTheory): inductive construction of composable arrows (#8146)
Added CategoryTheory.Nerve.δ₀_eqView on Github →