Documentation Verification Report

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` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types`	`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` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	`hasDimensionLT_prod`
`hasDimensionLT_prod` 📖	mathematical	—	`HasDimensionLT` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	`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` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `N` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `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` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.flip`	—	`finite_of_isPullback` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.IsPullback.of_hasPullback`
`instFiniteTensorObj` 📖	mathematical	—	`Finite` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	`hasDimensionLT_of_finite` `finite_of_hasDimensionLT` `instHasDimensionLTTensorObjHAddNat` `Subtype.finite` `instFiniteObjOppositeSimplexCategoryTensorObj` `instFiniteObjOppositeSimplexCategoryOfFinite`
`instHasDimensionLETensorObjHAddNat` 📖	mathematical	—	`HasDimensionLE` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	`hasDimensionLE_prod`
`instHasDimensionLTTensorObjHAddNat` 📖	mathematical	—	`HasDimensionLT` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	`hasDimensionLT_prod`

SSet.Subcomplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofSimplexProd_eq_range` 📖	mathematical	—	`prod` `ofSimplex` `range` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `DFunLike.coe` `Equiv` `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