FiniteProd

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

Statistics

Metric	Count
Definitions	0
Theorems ofSimplexProd_eq_range, finite_of_isPullback, hasDimensionLE_prod, hasDimensionLT_prod, iSup_subcomplexOfSimplex_prod_eq_top, instFinitePullback, instFiniteTensorObj, instHasDimensionLETensorObjHAddNat, instHasDimensionLTTensorObjHAddNat	9
Total	9

SSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_of_isPullback 📖	mathematical	CategoryTheory.IsPullback SSet largeCategory	Finite	—	CategoryTheory.IsPullback.hom_ext CategoryTheory.CartesianMonoidalCategory.comp_lift CategoryTheory.CartesianMonoidalCategory.lift_fst CategoryTheory.eq_whisker CategoryTheory.CartesianMonoidalCategory.lift_snd finite_of_mono instFiniteTensorObj
hasDimensionLE_prod 📖	mathematical	—	HasDimensionLE CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory	—	hasDimensionLT_prod
hasDimensionLT_prod 📖	mathematical	—	HasDimensionLT CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory	—	hasDimensionLT_subcomplex_top_iff iSup_subcomplexOfSimplex_prod_eq_top Subcomplex.ofSimplexProd_eq_range dim_lt_of_nonDegenerate N.nonDegenerate hasDimensionLT_of_le prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat instHasDimensionLTToSSetRange
iSup_subcomplexOfSimplex_prod_eq_top 📖	mathematical	—	iSup Subcomplex CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory N ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Subcomplex.prod Subcomplex.ofSimplex S.dim N.toS S.simplex Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	CategoryTheory.Subfunctor.ext Set.ext CategoryTheory.Subfunctor.iSup_obj
instFinitePullback 📖	mathematical	—	Finite CategoryTheory.Limits.pullback SSet largeCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits hasLimits CategoryTheory.Limits.cospan	—	finite_of_isPullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits hasLimits CategoryTheory.IsPullback.of_hasPullback
instFiniteTensorObj 📖	mathematical	—	Finite CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory	—	hasDimensionLT_of_finite finite_of_hasDimensionLT instHasDimensionLTTensorObjHAddNat Subtype.finite instFiniteObjOppositeSimplexCategoryTensorObj instFiniteObjOppositeSimplexCategoryOfFinite
instHasDimensionLETensorObjHAddNat 📖	mathematical	—	HasDimensionLE CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory	—	hasDimensionLE_prod
instHasDimensionLTTensorObjHAddNat 📖	mathematical	—	HasDimensionLT CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory	—	hasDimensionLT_prod

SSet.Subcomplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofSimplexProd_eq_range 📖	mathematical	—	prod ofSimplex range CategoryTheory.MonoidalCategoryStruct.tensorObj SSet SSet.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.MonoidalCategoryStruct.tensorHom DFunLike.coe Equiv Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm SSet.yonedaEquiv	—	range_tensorHom range_eq_ofSimplex Equiv.apply_symm_apply

---

← Back to Index