TopologicalSimplex

📁 Source: Mathlib/AlgebraicTopology/TopologicalSimplex.lean

Statistics

Metric	Count
Definitions instUniqueCarrierObjTopCatToTopMkOfNatNat, instUniqueCarrierObjTopCatToTop₀MkOfNatNat, toTop, toTopMap, toTopObj, toTopObjOneHomeo, toTop₀	7
Theorems coe_toTopMap, continuous_toTopMap, instNonemptyCarrierObjTopCatToTop, instNonemptyCarrierObjTopCatToTop₀, instPathConnectedSpaceCarrierObjTopCatToTop, instPathConnectedSpaceCarrierObjTopCatToTop₀, ext, toTopObj_one_add_eq_one, toTopObj_one_coe_add_coe_eq_one, toTopObj_zero_apply_zero, toTop_map, toTop_obj, toTop₀_map, toTop₀_obj	14
Total	21

SimplexCategory

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toTopMap 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module LinearMap.instFunLike FunOnFinite.linearMap Finite.of_fintype Finset.sum Finset.filter Finset.univ	—	FunOnFinite.linearMap_apply_apply
continuous_toTopMap 📖	mathematical	—	Continuous Set.Elem stdSimplex instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace stdSimplex.map	—	stdSimplex.continuous_map
instNonemptyCarrierObjTopCatToTop 📖	mathematical	—	TopCat.carrier CategoryTheory.Functor.obj SimplexCategory smallCategory TopCat TopCat.instCategory toTop	—	ULift.instNonempty_mathlib instNonemptyCarrierObjTopCatToTop₀
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
toTopObj_one_add_eq_one 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe Set.Elem stdSimplex Fin.fintype stdSimplex.instFunLikeElemForall AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	stdSimplex.add_eq_one
toTopObj_one_coe_add_coe_eq_one 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe Set.Elem stdSimplex Fin.fintype stdSimplex.instFunLikeElemForall AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	stdSimplex.add_eq_one
toTopObj_zero_apply_zero 📖	mathematical	—	DFunLike.coe Set.Elem stdSimplex stdSimplex.instFunLikeElemForall AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	stdSimplex.eq_one_of_unique
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 OrderHom.instFunLike CategoryTheory.ConcreteCategory.hom 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	—	—

SimplexCategory.toTopObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	DFunLike.coe Set.Elem stdSimplex stdSimplex.instFunLikeElemForall	—	—	stdSimplex.ext

---

← Back to Index