Monoidal

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

Statistics

Metric	Count
Definitions `prod`, `prodIso`, `unionProd`, `symmIso`, `ι₁`, `ι₂`, `instMonoidalTruncation`, `isTerminalObj₀`, `unitHomEquiv`, `ι₀`, `ι₁`	11
Theorems `mem_unionProd_iff`, `prodIso_hom`, `prodIso_inv`, `prod_le_prod_top`, `prod_le_top_prod`, `prod_le_unionProd`, `prod_monotone`, `prod_obj`, `prod_top_le_unionProd`, `range_tensorHom`, `top_prod_le_unionProd`, `bicartSq`, `image_β_hom`, `image_β_inv`, `isPushout`, `preimage_β_hom`, `preimage_β_inv`, `symmIso_hom`, `symmIso_inv`, `ι₁_ι`, `ι₁_ι_assoc`, `ι₂_ι`, `ι₂_ι_assoc`, `tensor_map_apply_fst`, `tensor_map_apply_snd`, `associator_hom_app_apply`, `associator_inv_app_apply`, `instFiniteObjOppositeSimplexCategoryTensorObj`, `instFiniteTensorUnit`, `instHasDimensionLETensorUnitOfNatNat`, `leftUnitor_hom_app_apply`, `leftUnitor_inv_app_apply`, `prod_map_fst`, `prod_map_snd`, `prod_δ_fst`, `prod_δ_snd`, `prod_σ_fst`, `prod_σ_snd`, `rightUnitor_hom_app_apply`, `rightUnitor_inv_app_apply`, `ext₀`, `ext₀_iff`, `tensorHom_app_apply`, `whiskerLeft_app_apply`, `whiskerRight_app_apply`, `ι₀_app_fst`, `ι₀_app_snd_apply`, `ι₀_comp`, `ι₀_comp_assoc`, `ι₀_fst`, `ι₀_fst_assoc`, `ι₀_snd`, `ι₀_snd_assoc`, `ι₁_app_fst`, `ι₁_app_snd_apply`, `ι₁_comp`, `ι₁_comp_assoc`, `ι₁_fst`, `ι₁_fst_assoc`, `ι₁_snd`, `ι₁_snd_assoc`	61
Total	72

SSet

Definitions

Name	Category	Theorems
`unitHomEquiv` 📖	CompOp	—
`ι₀` 📖	CompOp	14 math math: `ι₀_snd_assoc`, `RelativeMorphism.Homotopy.h₀_assoc`, `stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assoc`, `ι₀_fst_assoc`, `ι₀_snd`, `Homotopy.h₀`, `ι₀_comp_assoc`, `ι₀_comp`, `Homotopy.h₀_assoc`, `ι₀_app_snd_apply`, `RelativeMorphism.Homotopy.h₀`, `ι₀_fst`, `stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ`, `ι₀_app_fst`
`ι₁` 📖	CompOp	14 math math: `stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ`, `Homotopy.h₁_assoc`, `ι₁_app_snd_apply`, `ι₁_comp`, `ι₁_snd_assoc`, `ι₁_app_fst`, `ι₁_snd`, `Homotopy.h₁`, `RelativeMorphism.Homotopy.h₁_assoc`, `ι₁_fst`, `RelativeMorphism.Homotopy.h₁`, `ι₁_fst_assoc`, `stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assoc`, `ι₁_comp_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_hom_app_apply` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.Functor.obj`	—	—
`associator_inv_app_apply` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.Functor.obj`	—	—
`instFiniteObjOppositeSimplexCategoryTensorObj` 📖	mathematical	—	`Finite` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	—
`instFiniteTensorUnit` 📖	mathematical	—	`Finite` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	`finite_of_iso` `stdSimplex.instFiniteObjSimplexCategory`
`instHasDimensionLETensorUnitOfNatNat` 📖	mathematical	—	`HasDimensionLE` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `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_iff_of_iso` `stdSimplex.instHasDimensionLEObjSimplexCategoryMk`
`leftUnitor_hom_app_apply` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.Functor.obj`	—	—
`leftUnitor_inv_app_apply` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.Functor.obj`	—	—
`prod_map_fst` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	—
`prod_map_snd` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	—
`prod_δ_fst` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `CategoryTheory.SimplicialObject.δ` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	—
`prod_δ_snd` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `CategoryTheory.SimplicialObject.δ` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	—
`prod_σ_fst` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `CategoryTheory.SimplicialObject.σ` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	—
`prod_σ_snd` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `CategoryTheory.SimplicialObject.σ` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	—
`rightUnitor_hom_app_apply` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `CategoryTheory.Functor.obj`	—	—
`rightUnitor_inv_app_apply` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `CategoryTheory.Functor.obj`	—	—
`tensorHom_app_apply` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `CategoryTheory.Functor.obj`	—	—
`whiskerLeft_app_apply` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Functor.obj`	—	—
`whiskerRight_app_apply` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.Functor.obj`	—	—
`ι₀_app_fst` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `stdSimplex` `CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `ι₀`	—	—
`ι₀_app_snd_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `stdSimplex` `Opposite.op` `stdSimplex.instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat` `CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `ι₀`	—	—
`ι₀_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `stdSimplex` `ι₀` `CategoryTheory.MonoidalCategoryStruct.whiskerRight`	—	—
`ι₀_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `stdSimplex` `ι₀` `CategoryTheory.MonoidalCategoryStruct.whiskerRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₀_comp`
`ι₀_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `stdSimplex` `ι₀` `CategoryTheory.SemiCartesianMonoidalCategory.fst` `CategoryTheory.Functor.cartesianMonoidalCategory` `CategoryTheory.CategoryStruct.id`	—	—
`ι₀_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `stdSimplex` `ι₀` `CategoryTheory.SemiCartesianMonoidalCategory.fst` `CategoryTheory.Functor.cartesianMonoidalCategory`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₀_fst`
`ι₀_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `stdSimplex` `ι₀` `CategoryTheory.SemiCartesianMonoidalCategory.snd` `CategoryTheory.Functor.cartesianMonoidalCategory` `const` `DFunLike.coe` `Equiv` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `stdSimplex.obj₀Equiv`	—	—
`ι₀_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `stdSimplex` `ι₀` `CategoryTheory.SemiCartesianMonoidalCategory.snd` `CategoryTheory.Functor.cartesianMonoidalCategory` `const` `DFunLike.coe` `Equiv` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `stdSimplex.obj₀Equiv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₀_snd`
`ι₁_app_fst` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `stdSimplex` `CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `ι₁`	—	—
`ι₁_app_snd_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet` `CategoryTheory.Functor.category` `stdSimplex` `Opposite.op` `stdSimplex.instFunLikeObjOppositeSimplexCategoryMkOpFinHAddNatOfNat` `CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `ι₁`	—	—
`ι₁_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `stdSimplex` `ι₁` `CategoryTheory.MonoidalCategoryStruct.whiskerRight`	—	—
`ι₁_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `stdSimplex` `ι₁` `CategoryTheory.MonoidalCategoryStruct.whiskerRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₁_comp`
`ι₁_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `stdSimplex` `ι₁` `CategoryTheory.SemiCartesianMonoidalCategory.fst` `CategoryTheory.Functor.cartesianMonoidalCategory` `CategoryTheory.CategoryStruct.id`	—	—
`ι₁_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `stdSimplex` `ι₁` `CategoryTheory.SemiCartesianMonoidalCategory.fst` `CategoryTheory.Functor.cartesianMonoidalCategory`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₁_fst`
`ι₁_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `stdSimplex` `ι₁` `CategoryTheory.SemiCartesianMonoidalCategory.snd` `CategoryTheory.Functor.cartesianMonoidalCategory` `const` `DFunLike.coe` `Equiv` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `stdSimplex.obj₀Equiv`	—	—
`ι₁_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `CategoryTheory.Functor.obj` `stdSimplex` `ι₁` `CategoryTheory.SemiCartesianMonoidalCategory.snd` `CategoryTheory.Functor.cartesianMonoidalCategory` `const` `DFunLike.coe` `Equiv` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `stdSimplex.obj₀Equiv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₁_snd`

SSet.Subcomplex

Definitions

Name	Category	Theorems
`prod` 📖	CompOp	13 math math: `prod_top_le_unionProd`, `prodIso_hom`, `SSet.iSup_subcomplexOfSimplex_prod_eq_top`, `ofSimplexProd_eq_range`, `prod_obj`, `prod_le_unionProd`, `prod_monotone`, `prodIso_inv`, `prod_le_top_prod`, `unionProd.bicartSq`, `range_tensorHom`, `top_prod_le_unionProd`, `prod_le_prod_top`
`prodIso` 📖	CompOp	2 math math: `prodIso_hom`, `prodIso_inv`
`unionProd` 📖	CompOp	16 math math: `prod_top_le_unionProd`, `mem_unionProd_iff`, `unionProd.isPushout`, `unionProd.image_β_inv`, `unionProd.symmIso_inv`, `unionProd.image_β_hom`, `unionProd.symmIso_hom`, `unionProd.ι₂_ι`, `unionProd.ι₁_ι`, `prod_le_unionProd`, `unionProd.ι₁_ι_assoc`, `unionProd.ι₂_ι_assoc`, `unionProd.preimage_β_inv`, `unionProd.preimage_β_hom`, `unionProd.bicartSq`, `top_prod_le_unionProd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_unionProd_iff` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `unionProd`	—	—
`prodIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `toSSet` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `prod` `prodIso` `CategoryTheory.CartesianMonoidalCategory.lift` `CategoryTheory.Functor.cartesianMonoidalCategory` `lift` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `ι` `CategoryTheory.SemiCartesianMonoidalCategory.fst` `CategoryTheory.SemiCartesianMonoidalCategory.snd`	—	—
`prodIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `toSSet` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `prod` `prodIso` `lift` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `ι`	—	—
`prod_le_prod_top` 📖	mathematical	—	`SSet.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` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `prod` `Top.top` `OrderTop.toTop` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`prod_monotone` `le_refl` `le_top`
`prod_le_top_prod` 📖	mathematical	—	`SSet.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` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `prod` `Top.top` `OrderTop.toTop` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`prod_monotone` `le_top` `le_refl`
`prod_le_unionProd` 📖	mathematical	—	`SSet.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` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `prod` `unionProd`	—	`LE.le.trans` `prod_le_prod_top` `prod_top_le_unionProd`
`prod_monotone` 📖	mathematical	`SSet.Subcomplex` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory`	`SSet.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` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `prod`	—	—
`prod_obj` 📖	mathematical	—	`CategoryTheory.Subfunctor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet` `CategoryTheory.Functor.category` `CategoryTheory.types` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `prod` `Set.prod` `CategoryTheory.Functor.obj`	—	—
`prod_top_le_unionProd` 📖	mathematical	—	`SSet.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` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `prod` `Top.top` `OrderTop.toTop` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `unionProd`	—	`le_sup_right`
`range_tensorHom` 📖	mathematical	—	`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.MonoidalCategoryStruct.tensorHom` `prod`	—	`CategoryTheory.Subfunctor.ext` `Set.ext` `Prod.eq_iff_fst_eq_snd_eq`
`top_prod_le_unionProd` 📖	mathematical	—	`SSet.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` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `prod` `Top.top` `OrderTop.toTop` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `unionProd`	—	`le_sup_left`

SSet.Subcomplex.unionProd

Definitions

Name	Category	Theorems
`symmIso` 📖	CompOp	2 math math: `symmIso_inv`, `symmIso_hom`
`ι₁` 📖	CompOp	3 math math: `isPushout`, `ι₁_ι`, `ι₁_ι_assoc`
`ι₂` 📖	CompOp	3 math math: `isPushout`, `ι₂_ι`, `ι₂_ι_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bicartSq` 📖	mathematical	—	`SSet.Subcomplex.BicartSq` `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` `SSet.Subcomplex.prod` `Top.top` `SSet.Subcomplex` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `SSet.Subcomplex.unionProd`	—	`CategoryTheory.Subfunctor.ext` `Set.ext`
`image_β_hom` 📖	mathematical	—	`SSet.Subcomplex.image` `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.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Monoidal.functorCategoryMonoidal` `SSet.Subcomplex.unionProd` `CategoryTheory.Iso.hom` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.Monoidal.functorCategoryBraided` `CategoryTheory.instBraidedCategoryType`	—	`preimage_β_hom` `SSet.Subcomplex.preimage_image_of_isIso` `CategoryTheory.Iso.isIso_hom`
`image_β_inv` 📖	mathematical	—	`SSet.Subcomplex.image` `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.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Monoidal.functorCategoryMonoidal` `SSet.Subcomplex.unionProd` `CategoryTheory.Iso.inv` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.Monoidal.functorCategoryBraided` `CategoryTheory.instBraidedCategoryType`	—	`image_β_hom`
`isPushout` 📖	mathematical	—	`CategoryTheory.IsPushout` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `SSet.Subcomplex.toSSet` `SSet.Subcomplex.unionProd` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `SSet.Subcomplex.ι` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `ι₁` `ι₂`	—	`CategoryTheory.IsPushout.of_iso` `Lattice.BicartSq.le₁₂` `bicartSq` `Lattice.BicartSq.le₁₃` `Lattice.BicartSq.le₂₄` `Lattice.BicartSq.le₃₄` `SSet.Subcomplex.BicartSq.isPushout`
`preimage_β_hom` 📖	mathematical	—	`SSet.Subcomplex.preimage` `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.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Monoidal.functorCategoryMonoidal` `SSet.Subcomplex.unionProd` `CategoryTheory.Iso.hom` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.Monoidal.functorCategoryBraided` `CategoryTheory.instBraidedCategoryType`	—	`CategoryTheory.Subfunctor.ext` `Set.ext`
`preimage_β_inv` 📖	mathematical	—	`SSet.Subcomplex.preimage` `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.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Monoidal.functorCategoryMonoidal` `SSet.Subcomplex.unionProd` `CategoryTheory.Iso.inv` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.Monoidal.functorCategoryBraided` `CategoryTheory.instBraidedCategoryType`	—	`preimage_β_hom`
`symmIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet.Subcomplex.toSSet` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `SSet.Subcomplex.unionProd` `symmIso` `SSet.Subcomplex.lift` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Monoidal.functorCategoryMonoidal` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `SSet.Subcomplex.ι` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.Monoidal.functorCategoryBraided` `CategoryTheory.instBraidedCategoryType`	—	—
`symmIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet.Subcomplex.toSSet` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `SSet.Subcomplex.unionProd` `symmIso` `SSet.Subcomplex.lift` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Monoidal.functorCategoryMonoidal` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `SSet.Subcomplex.ι` `CategoryTheory.Iso.hom` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.Monoidal.functorCategoryBraided` `CategoryTheory.instBraidedCategoryType`	—	—
`ι₁_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `SSet.Subcomplex.toSSet` `SSet.Subcomplex.unionProd` `ι₁` `SSet.Subcomplex.ι` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft`	—	—
`ι₁_ι_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `SSet.Subcomplex.toSSet` `SSet.Subcomplex.unionProd` `ι₁` `SSet.Subcomplex.ι` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₁_ι`
`ι₂_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `SSet.Subcomplex.toSSet` `SSet.Subcomplex.unionProd` `ι₂` `SSet.Subcomplex.ι` `CategoryTheory.MonoidalCategoryStruct.whiskerRight`	—	—
`ι₂_ι_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory` `SSet.Subcomplex.toSSet` `SSet.Subcomplex.unionProd` `ι₂` `SSet.Subcomplex.ι` `CategoryTheory.MonoidalCategoryStruct.whiskerRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₂_ι`

SSet.Truncated

Definitions

Name	Category	Theorems
`instMonoidalTruncation` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tensor_map_apply_fst` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet.Truncated` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	—
`tensor_map_apply_snd` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SSet.Truncated` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.typesCartesianMonoidalCategory`	—	—

SSet.stdSimplex

Definitions

Name	Category	Theorems
`isTerminalObj₀` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext₀` 📖	—	—	—	—	`CategoryTheory.Limits.IsTerminal.hom_ext`
`ext₀_iff` 📖	—	—	—	—	`ext₀`

---

← Back to Index