TopologicalSimplex

📁 Source: Mathlib/AlgebraicTopology/TopologicalSimplex.lean

Statistics

Metric	Count
Definitions instUniqueCarrierObjTopCatToTopMkOfNatNat, instUniqueCarrierObjTopCatToTop₀MkOfNatNat, toTop, toTop₀	4
Theorems instNonemptyCarrierObjTopCatToTop, instNonemptyCarrierObjTopCatToTop₀, instPathConnectedSpaceCarrierObjTopCatToTop, instPathConnectedSpaceCarrierObjTopCatToTop₀, toTop_map, toTop_obj, toTop₀_map, toTop₀_obj	8
Total	12

SimplexCategory

Definitions

Name	Category	Theorems
instUniqueCarrierObjTopCatToTopMkOfNatNat 📖	CompOp	—
instUniqueCarrierObjTopCatToTop₀MkOfNatNat 📖	CompOp	—
toTop 📖	CompOp	5 math math: instPathConnectedSpaceCarrierObjTopCatToTop, instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex, toTop_obj, toTop_map, instNonemptyCarrierObjTopCatToTop
toTop₀ 📖	CompOp	4 math math: instNonemptyCarrierObjTopCatToTop₀, instPathConnectedSpaceCarrierObjTopCatToTop₀, toTop₀_map, toTop₀_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNonemptyCarrierObjTopCatToTop 📖	mathematical	—	TopCat.carrier CategoryTheory.Functor.obj SimplexCategory smallCategory TopCat TopCat.instCategory toTop	—	—
instNonemptyCarrierObjTopCatToTop₀ 📖	mathematical	—	TopCat.carrier CategoryTheory.Functor.obj SimplexCategory smallCategory TopCat TopCat.instCategory toTop₀	—	stdSimplex.instNonemptyElemForall Real.instIsOrderedRing
instPathConnectedSpaceCarrierObjTopCatToTop 📖	mathematical	—	PathConnectedSpace TopCat.carrier CategoryTheory.Functor.obj SimplexCategory smallCategory TopCat TopCat.instCategory toTop TopCat.str	—	Function.Surjective.pathConnectedSpace instPathConnectedSpaceCarrierObjTopCatToTop₀ ULift.up_surjective continuous_uliftUp
instPathConnectedSpaceCarrierObjTopCatToTop₀ 📖	mathematical	—	PathConnectedSpace TopCat.carrier CategoryTheory.Functor.obj SimplexCategory smallCategory TopCat TopCat.instCategory toTop₀ TopCat.str	—	instPathConnectedSpaceElemForallRealStdSimplexOfNonempty
toTop_map 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategory smallCategory TopCat TopCat.instCategory toTop TopCat.uliftFunctor TopCat.of Set.Elem stdSimplex Real len Real.semiring Real.partialOrder instFintypeToTypeOrderHomFinHAddNatLenOfNat instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace TopCat.ofHom stdSimplex.map Real.instIsOrderedRing DFunLike.coe OrderHom PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ConcreteCategory.hom OrderHom.instFunLike instConcreteCategoryOrderHomFinHAddNatLenOfNat	—	—
toTop_obj 📖	mathematical	—	CategoryTheory.Functor.obj SimplexCategory smallCategory TopCat TopCat.instCategory toTop TopCat.uliftFunctor TopCat.of Set.Elem stdSimplex Real len Real.semiring Real.partialOrder instFintypeToTypeOrderHomFinHAddNatLenOfNat instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	—
toTop₀_map 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategory smallCategory TopCat TopCat.instCategory toTop₀ TopCat.ofHom Set.Elem stdSimplex Real len Real.semiring Real.partialOrder instFintypeToTypeOrderHomFinHAddNatLenOfNat instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stdSimplex.map Real.instIsOrderedRing DFunLike.coe CategoryTheory.ConcreteCategory.hom OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike instConcreteCategoryOrderHomFinHAddNatLenOfNat	—	—
toTop₀_obj 📖	mathematical	—	CategoryTheory.Functor.obj SimplexCategory smallCategory TopCat TopCat.instCategory toTop₀ TopCat.of Set.Elem stdSimplex Real len Real.semiring Real.partialOrder instFintypeToTypeOrderHomFinHAddNatLenOfNat instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	—

---

← Back to Index