SingularSet

📁 Source: Mathlib/AlgebraicTopology/SingularSet.lean

Statistics

Metric	Count
Definitions toTop, toTopSimplex, toSSet, toSSetIsoConst, toSSetObjEquiv, sSetTopAdj	6
Theorems instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex	1
Total	7

SSet

Definitions

Name	Category	Theorems
toTop 📖	CompOp	1 math math: instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex
toTopSimplex 📖	CompOp	1 math math: instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex

TopCat

Definitions

Name	Category	Theorems
toSSet 📖	CompOp	—
toSSetIsoConst 📖	CompOp	—
toSSetObjEquiv 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
sSetTopAdj 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex 📖	mathematical	—	CategoryTheory.Functor.IsLeftKanExtension SimplexCategory TopCat SSet SimplexCategory.smallCategory TopCat.instCategory SSet.largeCategory SSet.toTop SSet.stdSimplex SimplexCategory.toTop CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp SSet.toTopSimplex	—	CategoryTheory.Functor.instHasLeftKanExtension CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape UnivLE.small UnivLE.self CategoryTheory.Functor.instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit

---

← Back to Index