StrictSegal

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean

Statistics

Metric	Count
Definitions strictSegal, IsStrictSegal, StrictSegal, ofCore, ofIsStrictSegal, spineEquiv, spineToDiagonal, spineToSimplex, truncation, StrictSegalCore, concat, spineToSimplex, spineToSimplexAux, IsStrictSegal, StrictSegal, ofIsStrictSegal, spineEquiv, spineToDiagonal, spineToSimplex	19
Theorems isStrictSegal, segal, instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal, isStrictSegal, spineInjective, spineToSimplex_arrow, spineToSimplex_edge, spineToSimplex_interval, spineToSimplex_map, spineToSimplex_spine, spineToSimplex_spine_apply, spineToSimplex_vertex, spine_spineToSimplex, spine_spineToSimplex_apply, spine_δ_arrow_eq, spine_δ_arrow_gt, spine_δ_arrow_lt, spine_δ_vertex_ge, spine_δ_vertex_lt, injective, map_mkOfSucc_zero_concat, map_mkOfSucc_zero_spineToSimplex, spineToSimplex_spine, spineToSimplex_succ, spineToSimplex_zero, spine_spineToSimplex, δ₀_concat, δ₀_spineToSimplex, ext, hom_ext, segal, spine_bijective, isStrictSegal, spineInjective, spineToSimplex_arrow, spineToSimplex_edge, spineToSimplex_interval, spineToSimplex_map, spineToSimplex_spine, spineToSimplex_spine_apply, spineToSimplex_vertex, spine_spineToSimplex, spine_spineToSimplex_apply, spine_δ_arrow_eq, spine_δ_arrow_gt, spine_δ_arrow_lt, spine_δ_vertex_ge, spine_δ_vertex_lt, spine_injective, spine_surjective	50
Total	69

CategoryTheory.Nerve

Definitions

Name	Category	Theorems
strictSegal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStrictSegal 📖	mathematical	—	SSet.IsStrictSegal CategoryTheory.nerve	—	SSet.StrictSegal.isStrictSegal

SSet

Definitions

Name	Category	Theorems
IsStrictSegal 📖	CompData	2 math math: CategoryTheory.Nerve.isStrictSegal, StrictSegal.isStrictSegal
StrictSegal 📖	CompData	—
StrictSegalCore 📖	CompData	—

SSet.IsStrictSegal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
segal 📖	mathematical	—	Function.Bijective CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op SSet.Path SSet.spine	—	—

SSet.StrictSegal

Definitions

Name	Category	Theorems
ofCore 📖	CompOp	—
ofIsStrictSegal 📖	CompOp	—
spineEquiv 📖	CompOp	1 math math: spineInjective
spineToDiagonal 📖	CompOp	2 math math: spine_δ_arrow_eq, spineToSimplex_edge
spineToSimplex 📖	CompOp	14 math math: spine_δ_arrow_eq, spine_δ_arrow_lt, spineToSimplex_map, spineToSimplex_interval, spineToSimplex_spine, spineToSimplex_edge, spine_δ_arrow_gt, spine_spineToSimplex_apply, spineToSimplex_spine_apply, spineToSimplex_arrow, spine_spineToSimplex, spine_δ_vertex_lt, spine_δ_vertex_ge, spineToSimplex_vertex
truncation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal 📖	mathematical	—	SSet.Truncated.IsStrictSegal CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.Truncated SSet.Truncated.largeCategory SSet.truncation	—	SSet.Truncated.StrictSegal.isStrictSegal
isStrictSegal 📖	mathematical	—	SSet.IsStrictSegal	—	Equiv.bijective
spineInjective 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op SSet.Path DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike spineEquiv	—	Equiv.injective
spineToSimplex_arrow 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.mkOfSucc spineToSimplex SSet.Path.arrow	—	SSet.spine_arrow spine_spineToSimplex_apply
spineToSimplex_edge 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.intervalEdge spineToSimplex spineToDiagonal SSet.Path.interval	—	spineToSimplex_interval CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.diag_subinterval_eq
spineToSimplex_interval 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.subinterval spineToSimplex SSet.Path.interval	—	spineInjective spine_spineToSimplex_apply SSet.spine_map_subinterval
spineToSimplex_map 📖	mathematical	—	spineToSimplex SSet.Path.map CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op	—	spineInjective SSet.Path.ext' CategoryTheory.types_comp_apply CategoryTheory.NatTrans.naturality spineToSimplex_arrow SSet.Path.map_arrow
spineToSimplex_spine 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op SSet.Path spineToSimplex SSet.spine	—	—
spineToSimplex_spine_apply 📖	mathematical	—	spineToSimplex SSet.spine	—	spineToSimplex_spine
spineToSimplex_vertex 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.const spineToSimplex SSet.Path.vertex	—	SSet.spine_vertex spine_spineToSimplex_apply
spine_spineToSimplex 📖	mathematical	—	SSet.Path CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op SSet.spine spineToSimplex	—	—
spine_spineToSimplex_apply 📖	mathematical	—	SSet.spine spineToSimplex	—	spine_spineToSimplex
spine_δ_arrow_eq 📖	mathematical	—	SSet.Path.arrow SSet.spine CategoryTheory.SimplicialObject.δ CategoryTheory.types spineToSimplex spineToDiagonal SSet.Path.interval	—	CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.mkOfSucc_δ_eq spineToSimplex_edge
spine_δ_arrow_gt 📖	mathematical	—	SSet.Path.arrow SSet.spine CategoryTheory.SimplicialObject.δ CategoryTheory.types spineToSimplex	—	CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.mkOfSucc_δ_gt spineToSimplex_arrow
spine_δ_arrow_lt 📖	mathematical	—	SSet.Path.arrow SSet.spine CategoryTheory.SimplicialObject.δ CategoryTheory.types spineToSimplex	—	CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.mkOfSucc_δ_lt spineToSimplex_arrow
spine_δ_vertex_ge 📖	mathematical	—	SSet.Path.vertex SSet.spine CategoryTheory.SimplicialObject.δ CategoryTheory.types spineToSimplex	—	CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.const_comp spineToSimplex_vertex Fin.succAbove_of_le_castSucc
spine_δ_vertex_lt 📖	mathematical	—	SSet.Path.vertex SSet.spine CategoryTheory.SimplicialObject.δ CategoryTheory.types spineToSimplex	—	CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.const_comp spineToSimplex_vertex Fin.succAbove_of_castSucc_lt

SSet.StrictSegalCore

Definitions

Name	Category	Theorems
concat 📖	CompOp	3 math math: map_mkOfSucc_zero_concat, δ₀_concat, spineToSimplex_succ
spineToSimplex 📖	CompOp	6 math math: spineToSimplex_zero, map_mkOfSucc_zero_spineToSimplex, spineToSimplex_succ, δ₀_spineToSimplex, spine_spineToSimplex, spineToSimplex_spine
spineToSimplexAux 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective 📖	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.mkOfSucc CategoryTheory.SimplicialObject.δ	—	—	—
map_mkOfSucc_zero_concat 📖	mathematical	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.const SimplexCategory.len SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat	SimplexCategory.mkOfSucc concat	—	—
map_mkOfSucc_zero_spineToSimplex 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.mkOfSucc spineToSimplex SSet.Path.arrow	—	spineToSimplex_succ map_mkOfSucc_zero_concat
spineToSimplex_spine 📖	mathematical	—	spineToSimplex SSet.spine	—	SimplexCategory.const_eq_id CategoryTheory.FunctorToTypes.map_id_apply injective map_mkOfSucc_zero_spineToSimplex δ₀_spineToSimplex SSet.spine_δ₀
spineToSimplex_succ 📖	mathematical	—	spineToSimplex concat SSet.Path.arrow SSet.Path.interval	—	—
spineToSimplex_zero 📖	mathematical	—	spineToSimplex SSet.Path.vertex	—	—
spine_spineToSimplex 📖	mathematical	—	SSet.spine spineToSimplex	—	Subtype.prop
δ₀_concat 📖	mathematical	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.const SimplexCategory.len SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat	concat	—	—
δ₀_spineToSimplex 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types spineToSimplex SSet.Path.interval	—	spineToSimplex_succ δ₀_concat

SSet.Truncated

Definitions

Name	Category	Theorems
IsStrictSegal 📖	CompData	3 math math: CategoryTheory.Nerve.instIsStrictSegalObjCatTruncatedOfNatNatNerveFunctor₂, StrictSegal.isStrictSegal, SSet.StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal
StrictSegal 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spine_injective 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op Path spine	—	Function.Bijective.injective IsStrictSegal.spine_bijective
spine_surjective 📖	mathematical	—	spine	—	Function.Bijective.surjective IsStrictSegal.spine_bijective

SSet.Truncated.IsStrictSegal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	SimplexCategory.len CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.Hom.tr SimplexCategory.mkOfSucc	—	—	SSet.Truncated.spine_injective SSet.Truncated.Path.ext'
hom_ext 📖	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op	—	—	SSet.Truncated.hom_ext CategoryTheory.types_ext SimplexCategory.δ_comp_σ_self CategoryTheory.FunctorToTypes.map_id_apply ext
segal 📖	mathematical	—	Function.Bijective CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op SSet.Truncated.Path SSet.Truncated.spine	—	spine_bijective
spine_bijective 📖	mathematical	—	Function.Bijective CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op SSet.Truncated.Path SSet.Truncated.spine	—	—

SSet.Truncated.StrictSegal

Definitions

Name	Category	Theorems
ofIsStrictSegal 📖	CompOp	—
spineEquiv 📖	CompOp	3 math math: spineInjective, SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_one, SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_zero
spineToDiagonal 📖	CompOp	2 math math: spineToSimplex_edge, spine_δ_arrow_eq
spineToSimplex 📖	CompOp	14 math math: spine_spineToSimplex, spineToSimplex_spine, spineToSimplex_spine_apply, spine_δ_arrow_lt, spine_δ_arrow_gt, spineToSimplex_vertex, spine_δ_vertex_ge, spineToSimplex_edge, spineToSimplex_arrow, spine_δ_arrow_eq, spineToSimplex_interval, spine_spineToSimplex_apply, spine_δ_vertex_lt, spineToSimplex_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStrictSegal 📖	mathematical	—	SSet.Truncated.IsStrictSegal	—	Equiv.bijective
spineInjective 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op SSet.Truncated.Path DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike spineEquiv	—	Equiv.injective
spineToSimplex_arrow 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.Hom.tr SimplexCategory.mkOfSucc spineToSimplex SSet.Truncated.Path.arrow	—	SSet.Truncated.spine_arrow spine_spineToSimplex_apply
spineToSimplex_edge 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.Hom.tr SimplexCategory.intervalEdge spineToSimplex spineToDiagonal SSet.Truncated.Path.interval	—	spineToSimplex_interval CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.Truncated.Hom.tr_comp SimplexCategory.diag_subinterval_eq
spineToSimplex_interval 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.Hom.tr SimplexCategory.subinterval spineToSimplex SSet.Truncated.Path.interval	—	spineInjective spine_spineToSimplex_apply SSet.Truncated.spine_map_subinterval
spineToSimplex_map 📖	mathematical	—	spineToSimplex SSet.Truncated.Path.map CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op	—	spineInjective SSet.Truncated.Path.ext' CategoryTheory.types_comp_apply CategoryTheory.NatTrans.naturality spineToSimplex_arrow
spineToSimplex_spine 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op SSet.Truncated.Path spineToSimplex SSet.Truncated.spine	—	—
spineToSimplex_spine_apply 📖	mathematical	—	spineToSimplex SSet.Truncated.spine	—	spineToSimplex_spine
spineToSimplex_vertex 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.Hom.tr SimplexCategory.const spineToSimplex SSet.Truncated.Path.vertex	—	SSet.Truncated.spine_vertex spine_spineToSimplex_apply
spine_spineToSimplex 📖	mathematical	—	SSet.Truncated.Path CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op SSet.Truncated.spine spineToSimplex	—	—
spine_spineToSimplex_apply 📖	mathematical	—	SSet.Truncated.spine spineToSimplex	—	spine_spineToSimplex
spine_δ_arrow_eq 📖	mathematical	—	SSet.Truncated.Path.arrow SSet.Truncated.spine CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.Hom.tr SimplexCategory.δ spineToSimplex spineToDiagonal SSet.Truncated.Path.interval	—	SSet.Truncated.spine_arrow CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.Truncated.Hom.tr_comp SimplexCategory.mkOfSucc_δ_eq spineToSimplex_edge
spine_δ_arrow_gt 📖	mathematical	—	SSet.Truncated.Path.arrow SSet.Truncated.spine CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.Hom.tr SimplexCategory.δ spineToSimplex	—	SSet.Truncated.spine_arrow CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.Truncated.Hom.tr_comp SimplexCategory.mkOfSucc_δ_gt spineToSimplex_arrow
spine_δ_arrow_lt 📖	mathematical	—	SSet.Truncated.Path.arrow SSet.Truncated.spine CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.Hom.tr SimplexCategory.δ spineToSimplex	—	SSet.Truncated.spine_arrow CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.Truncated.Hom.tr_comp SimplexCategory.mkOfSucc_δ_lt spineToSimplex_arrow
spine_δ_vertex_ge 📖	mathematical	—	SSet.Truncated.Path.vertex SSet.Truncated.spine CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.Hom.tr SimplexCategory.δ spineToSimplex	—	SSet.Truncated.spine_vertex CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.Truncated.Hom.tr_comp SimplexCategory.const_comp spineToSimplex_vertex Fin.succAbove_of_le_castSucc
spine_δ_vertex_lt 📖	mathematical	—	SSet.Truncated.Path.vertex SSet.Truncated.spine CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.Hom.tr SimplexCategory.δ spineToSimplex	—	SSet.Truncated.spine_vertex CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.Truncated.Hom.tr_comp SimplexCategory.const_comp spineToSimplex_vertex Fin.succAbove_of_castSucc_lt

---

← Back to Index