Documentation Verification Report

Path

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

Statistics

Metric	Count
Definitions `arrow`, `interval`, `map`, `vertex`, `liftPath`, `arrow`, `interval`, `map`, `mk₂`, `vertex`, `Path₁`, `arrow`, `vertex`, `spine`, `spineId`, `spine`, `spineId`	17
Theorems `arrow_interval`, `arrow_src`, `arrow_tgt`, `congr_arrow`, `congr_vertex`, `ext`, `ext'`, `ext'_iff`, `ext_iff`, `ext₀`, `ext₀_iff`, `map_arrow`, `map_interval`, `map_vertex`, `liftPath_arrow_coe`, `liftPath_vertex_coe`, `map_ι_liftPath`, `arrow_src`, `arrow_tgt`, `ext`, `ext'`, `ext'_iff`, `ext_iff`, `map_arrow`, `map_interval`, `map_vertex`, `mk₂_arrow`, `mk₂_vertex`, `arrow_src`, `arrow_tgt`, `ext`, `ext_iff`, `spine_arrow`, `spine_map_subinterval`, `spine_map_vertex`, `spine_vertex`, `trunc_spine`, `spineId_arrow_coe`, `spineId_map_hornInclusion`, `spineId_vertex_coe`, `spine_arrow`, `spine_map_subinterval`, `spine_map_vertex`, `spine_vertex`, `spine_δ₀`, `spineId_arrow_apply_one`, `spineId_arrow_apply_zero`, `spineId_vertex`, `truncation_spine`	49
Total	66

SSet

Definitions

Name	Category	Theorems
`spine` 📖	CompOp	18 math math: `StrictSegal.spine_δ_arrow_eq`, `spine_map_subinterval`, `spine_vertex`, `StrictSegal.spine_δ_arrow_lt`, `spine_δ₀`, `spine_arrow`, `StrictSegal.spineToSimplex_spine`, `IsStrictSegal.segal`, `spine_map_vertex`, `StrictSegal.spine_δ_arrow_gt`, `StrictSegal.spine_spineToSimplex_apply`, `StrictSegal.spineToSimplex_spine_apply`, `StrictSegal.spine_spineToSimplex`, `truncation_spine`, `StrictSegal.spine_δ_vertex_lt`, `StrictSegalCore.spine_spineToSimplex`, `StrictSegal.spine_δ_vertex_ge`, `StrictSegalCore.spineToSimplex_spine`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`spine_arrow` 📖	mathematical	—	`Path.arrow` `spine` `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`	—	—
`spine_map_subinterval` 📖	mathematical	—	`spine` `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` `Path.interval`	—	`Truncated.spine_map_subinterval`
`spine_map_vertex` 📖	mathematical	—	`Path.vertex` `spine` `CategoryTheory.Functor.map` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `DFunLike.coe` `OrderHom` `SimplexCategory.len` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `SimplexCategory.Hom.toOrderHom`	—	`Truncated.spine_map_vertex`
`spine_vertex` 📖	mathematical	—	`Path.vertex` `spine` `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`	—	—
`spine_δ₀` 📖	mathematical	—	`spine` `CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `Path.interval`	—	`Path.ext₀` `SimplexCategory.const_eq_id` `CategoryTheory.FunctorToTypes.map_id_apply` `add_zero` `Path.ext'` `CategoryTheory.SimplicialObject.δ_def` `CategoryTheory.FunctorToTypes.map_comp_apply` `CategoryTheory.op_comp` `SimplexCategory.mkOfSucc_δ_gt` `Path.arrow_interval` `add_comm`
`truncation_spine` 📖	mathematical	—	`Truncated.spine` `CategoryTheory.Functor.obj` `SSet` `largeCategory` `Truncated` `Truncated.largeCategory` `truncation` `spine`	—	—

SSet.Path

Definitions

Name	Category	Theorems
`arrow` 📖	CompOp	17 math math: `SSet.StrictSegal.spine_δ_arrow_eq`, `SSet.StrictSegal.spine_δ_arrow_lt`, `SSet.stdSimplex.spineId_arrow_apply_zero`, `SSet.spine_arrow`, `ext_iff`, `arrow_tgt`, `map_arrow`, `congr_arrow`, `arrow_src`, `SSet.horn.spineId_arrow_coe`, `SSet.StrictSegal.spine_δ_arrow_gt`, `arrow_interval`, `SSet.stdSimplex.spineId_arrow_apply_one`, `SSet.StrictSegalCore.map_mkOfSucc_zero_spineToSimplex`, `SSet.StrictSegalCore.spineToSimplex_succ`, `SSet.StrictSegal.spineToSimplex_arrow`, `ext'_iff`
`interval` 📖	CompOp	9 math math: `SSet.StrictSegal.spine_δ_arrow_eq`, `SSet.spine_map_subinterval`, `map_interval`, `SSet.spine_δ₀`, `SSet.StrictSegal.spineToSimplex_interval`, `SSet.StrictSegal.spineToSimplex_edge`, `arrow_interval`, `SSet.StrictSegalCore.spineToSimplex_succ`, `SSet.StrictSegalCore.δ₀_spineToSimplex`
`map` 📖	CompOp	6 math math: `map_interval`, `SSet.horn.spineId_map_hornInclusion`, `SSet.StrictSegal.spineToSimplex_map`, `map_arrow`, `map_vertex`, `SSet.Subcomplex.map_ι_liftPath`
`vertex` 📖	CompOp	13 math math: `SSet.StrictSegalCore.spineToSimplex_zero`, `SSet.spine_vertex`, `ext_iff`, `arrow_tgt`, `congr_vertex`, `SSet.spine_map_vertex`, `arrow_src`, `ext₀_iff`, `SSet.stdSimplex.spineId_vertex`, `map_vertex`, `SSet.StrictSegal.spine_δ_vertex_lt`, `SSet.StrictSegal.spine_δ_vertex_ge`, `SSet.StrictSegal.spineToSimplex_vertex`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arrow_interval` 📖	mathematical	—	`arrow` `interval`	—	—
`arrow_src` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `arrow` `vertex`	—	`SSet.Truncated.Path.arrow_src`
`arrow_tgt` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `arrow` `vertex`	—	`SSet.Truncated.Path.arrow_tgt`
`congr_arrow` 📖	mathematical	—	`arrow`	—	—
`congr_vertex` 📖	mathematical	—	`vertex`	—	—
`ext` 📖	—	`vertex` `arrow`	—	—	`SSet.Truncated.Path.ext`
`ext'` 📖	—	`arrow`	—	—	`SSet.Truncated.Path.ext'`
`ext'_iff` 📖	mathematical	—	`arrow`	—	`ext'`
`ext_iff` 📖	mathematical	—	`vertex` `arrow`	—	`ext`
`ext₀` 📖	—	`vertex`	—	—	`ext` `Fintype.complete`
`ext₀_iff` 📖	mathematical	—	`vertex`	—	`ext₀`
`map_arrow` 📖	mathematical	—	`arrow` `map` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op`	—	—
`map_interval` 📖	mathematical	—	`interval` `map`	—	—
`map_vertex` 📖	mathematical	—	`vertex` `map` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op`	—	—

SSet.Subcomplex

Definitions

Name	Category	Theorems
`liftPath` 📖	CompOp	3 math math: `liftPath_arrow_coe`, `liftPath_vertex_coe`, `map_ι_liftPath`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`liftPath_arrow_coe` 📖	mathematical	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `SSet.Path.vertex` `SSet.Path.arrow`	`SimplexCategory.Truncated` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.len` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `SimplexCategory.Truncated.incl` `SSet.Truncated.Path₁.arrow` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.Truncated.trunc` `SSet` `SSet.largeCategory` `SSet.truncation` `toSSet` `liftPath`	—	—
`liftPath_vertex_coe` 📖	mathematical	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `SSet.Path.vertex` `SSet.Path.arrow`	`SimplexCategory.Truncated` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.len` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `SimplexCategory.Truncated.incl` `SSet.Truncated.Path₁.vertex` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.Truncated.trunc` `SSet` `SSet.largeCategory` `SSet.truncation` `toSSet` `liftPath`	—	—
`map_ι_liftPath` 📖	mathematical	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `SSet.Path.vertex` `SSet.Path.arrow`	`SSet.Path.map` `toSSet` `liftPath` `ι`	—	—

SSet.Truncated

Definitions

Name	Category	Theorems
`Path₁` 📖	CompData	—
`spine` 📖	CompOp	19 math math: `StrictSegal.spine_spineToSimplex`, `StrictSegal.spineToSimplex_spine`, `spine_map_subinterval`, `StrictSegal.spineToSimplex_spine_apply`, `StrictSegal.spine_δ_arrow_lt`, `spine_map_vertex`, `StrictSegal.spine_δ_arrow_gt`, `StrictSegal.spine_δ_vertex_ge`, `spine_arrow`, `spine_vertex`, `StrictSegal.spine_δ_arrow_eq`, `spine_surjective`, `trunc_spine`, `IsStrictSegal.spine_bijective`, `StrictSegal.spine_spineToSimplex_apply`, `SSet.truncation_spine`, `StrictSegal.spine_δ_vertex_lt`, `IsStrictSegal.segal`, `spine_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`spine_arrow` 📖	mathematical	—	`Path.arrow` `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.mkOfSucc`	—	—
`spine_map_subinterval` 📖	mathematical	—	`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.subinterval` `Path.interval`	—	`Path.ext` `CategoryTheory.FunctorToTypes.map_comp_apply` `CategoryTheory.op_comp` `SimplexCategory.Truncated.Hom.tr_comp` `lt_add_of_lt_add_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `SimplexCategory.const_subinterval_eq` `SimplexCategory.mkOfSucc_subinterval_eq`
`spine_map_vertex` 📖	mathematical	—	`Path.vertex` `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` `DFunLike.coe` `OrderHom` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `PartialOrder.toPreorder` `Fin.instPartialOrder` `OrderHom.instFunLike` `SimplexCategory.Hom.toOrderHom` `CategoryTheory.InducedCategory.Hom.hom`	—	`CategoryTheory.FunctorToTypes.map_comp_apply` `CategoryTheory.op_comp` `SimplexCategory.Truncated.Hom.tr_comp'` `SimplexCategory.const_comp`
`spine_vertex` 📖	mathematical	—	`Path.vertex` `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.const`	—	—
`trunc_spine` 📖	mathematical	—	`spine` `CategoryTheory.Functor.obj` `SSet.Truncated` `largeCategory` `trunc`	—	—

SSet.Truncated.Path

Definitions

Name	Category	Theorems
`arrow` 📖	CompOp	13 math math: `mk₂_arrow`, `map_arrow`, `ext_iff`, `SSet.Truncated.StrictSegal.spine_δ_arrow_lt`, `SSet.Truncated.StrictSegal.spine_δ_arrow_gt`, `SSet.Truncated.spine_arrow`, `SSet.Truncated.StrictSegal.spineToSimplex_arrow`, `arrow_src`, `SSet.Truncated.StrictSegal.spine_δ_arrow_eq`, `ext'_iff`, `arrow_tgt`, `SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_one`, `SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_zero`
`interval` 📖	CompOp	5 math math: `SSet.Truncated.spine_map_subinterval`, `SSet.Truncated.StrictSegal.spineToSimplex_edge`, `map_interval`, `SSet.Truncated.StrictSegal.spine_δ_arrow_eq`, `SSet.Truncated.StrictSegal.spineToSimplex_interval`
`map` 📖	CompOp	4 math math: `map_arrow`, `map_interval`, `map_vertex`, `SSet.Truncated.StrictSegal.spineToSimplex_map`
`mk₂` 📖	CompOp	2 math math: `mk₂_arrow`, `mk₂_vertex`
`vertex` 📖	CompOp	9 math math: `ext_iff`, `SSet.Truncated.spine_map_vertex`, `SSet.Truncated.StrictSegal.spineToSimplex_vertex`, `SSet.Truncated.StrictSegal.spine_δ_vertex_ge`, `SSet.Truncated.spine_vertex`, `arrow_src`, `map_vertex`, `arrow_tgt`, `SSet.Truncated.StrictSegal.spine_δ_vertex_lt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arrow_src` 📖	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.δ` `arrow` `vertex`	—	`SSet.Truncated.Path₁.arrow_src`
`arrow_tgt` 📖	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.δ` `arrow` `vertex`	—	`SSet.Truncated.Path₁.arrow_tgt`
`ext` 📖	—	`vertex` `arrow`	—	—	`SSet.Truncated.Path₁.ext`
`ext'` 📖	—	`arrow`	—	—	`ext` `Fin.eq_castSucc_or_eq_last` `arrow_src` `arrow_tgt`
`ext'_iff` 📖	mathematical	—	`arrow`	—	`ext'`
`ext_iff` 📖	mathematical	—	`vertex` `arrow`	—	`ext`
`map_arrow` 📖	mathematical	—	`arrow` `map` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op`	—	—
`map_interval` 📖	mathematical	—	`interval` `map`	—	—
`map_vertex` 📖	mathematical	—	`vertex` `map` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op`	—	—
`mk₂_arrow` 📖	mathematical	`vertex`	`SSet.Truncated.Path₁.arrow` `CategoryTheory.Functor.obj` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.Truncated.trunc` `mk₂` `Matrix.vecCons` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `SimplexCategory.Truncated.incl` `arrow` `Matrix.vecEmpty`	—	—
`mk₂_vertex` 📖	mathematical	`vertex`	`SSet.Truncated.Path₁.vertex` `CategoryTheory.Functor.obj` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.Truncated.trunc` `mk₂` `Matrix.vecCons` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `SimplexCategory.Truncated.incl` `Matrix.vecEmpty`	—	—

SSet.Truncated.Path₁

Definitions

Name	Category	Theorems
`arrow` 📖	CompOp	6 math math: `SSet.Truncated.Path.mk₂_arrow`, `ext_iff`, `SSet.horn.spineId_arrow_coe`, `SSet.Subcomplex.liftPath_arrow_coe`, `arrow_tgt`, `arrow_src`
`vertex` 📖	CompOp	6 math math: `ext_iff`, `SSet.horn.spineId_vertex_coe`, `arrow_tgt`, `SSet.Subcomplex.liftPath_vertex_coe`, `SSet.Truncated.Path.mk₂_vertex`, `arrow_src`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arrow_src` 📖	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.δ` `arrow` `vertex`	—	—
`arrow_tgt` 📖	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.δ` `arrow` `vertex`	—	—
`ext` 📖	—	`vertex` `arrow`	—	—	—
`ext_iff` 📖	mathematical	—	`vertex` `arrow`	—	`ext`

SSet.horn

Definitions

Name	Category	Theorems
`spineId` 📖	CompOp	3 math math: `spineId_map_hornInclusion`, `spineId_vertex_coe`, `spineId_arrow_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`spineId_arrow_coe` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `SimplexCategory.Truncated` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.len` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `SimplexCategory.Truncated.incl` `Opposite.op` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `SSet.horn` `SSet.Truncated.Path₁.arrow` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.Truncated.trunc` `SSet.truncation` `SSet.Subcomplex.toSSet` `spineId` `SSet.Path.arrow` `SSet.stdSimplex.spineId`	—	—
`spineId_map_hornInclusion` 📖	mathematical	—	`SSet.Path.map` `SSet.Subcomplex.toSSet` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `SSet.horn` `spineId` `SSet.Subcomplex.ι` `SSet.stdSimplex.spineId`	—	—
`spineId_vertex_coe` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `SimplexCategory.Truncated` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.len` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `SimplexCategory.Truncated.incl` `Opposite.op` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `SSet.horn` `SSet.Truncated.Path₁.vertex` `SSet.Truncated` `SSet.Truncated.largeCategory` `SSet.Truncated.trunc` `SSet.truncation` `SSet.Subcomplex.toSSet` `spineId` `SSet.stdSimplex.const`	—	—

SSet.stdSimplex

Definitions

Name	Category	Theorems
`spineId` 📖	CompOp	5 math math: `spineId_arrow_apply_zero`, `SSet.horn.spineId_map_hornInclusion`, `SSet.horn.spineId_arrow_coe`, `spineId_vertex`, `spineId_arrow_apply_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`spineId_arrow_apply_one` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `Opposite.op` `instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat` `SSet.Path.arrow` `spineId`	—	—
`spineId_arrow_apply_zero` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `Opposite.op` `instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat` `SSet.Path.arrow` `spineId`	—	—
`spineId_vertex` 📖	mathematical	—	`SSet.Path.vertex` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `spineId` `DFunLike.coe` `Equiv` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `obj₀Equiv`	—	—

---

← Back to Index