Documentation Verification Report

ProdStdSimplexOne

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

Statistics

Metric	Count
Definitions `nonDegenerateEquiv₁`	1
Theorems `nonDegenerateEquiv₁_fst`, `nonDegenerateEquiv₁_snd`	2
Total	3

SSet.prodStdSimplex

Definitions

Name	Category	Theorems
`nonDegenerateEquiv₁` 📖	CompOp	2 math math: `nonDegenerateEquiv₁_snd`, `nonDegenerateEquiv₁_fst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonDegenerateEquiv₁_fst` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `Set` `Set.instMembership` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `SSet.nonDegenerate` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `nonDegenerateEquiv₁` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `Equiv.symm` `SSet.stdSimplex.objEquiv` `SimplexCategory.σ`	—	—
`nonDegenerateEquiv₁_snd` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `SSet.stdSimplex` `Opposite.op` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `Set` `Set.instMembership` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `SSet.nonDegenerate` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `nonDegenerateEquiv₁` `SSet.stdSimplex.objMk₁`	—	—

---

← Back to Index