Documentation Verification Report

HornColimits

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

Statistics

Metric	Count
Definitions `isColimit`, `ι₀₁`, `ι₀₂`, `ι₀₁`, `ι₁₂`, `ι₀₂`, `ι₁₂`, `desc`, `multicofork`, `ι₀`, `ι₂`, `ι₃`, `desc`, `multicofork`, `ι₀`, `ι₁`, `ι₃`	17
Theorems `multicoequalizerDiagram`, `isPushout`, `sq`, `isPushout`, `sq`, `isPushout`, `sq`, `multicofork_pt`, `multicofork_π_three`, `multicofork_π_three_assoc`, `multicofork_π_two`, `multicofork_π_two_assoc`, `multicofork_π_zero`, `multicofork_π_zero_assoc`, `exists_desc`, `ι₀_desc`, `ι₀_desc_assoc`, `ι₂_desc`, `ι₂_desc_assoc`, `ι₃_desc`, `ι₃_desc_assoc`, `multicofork_pt`, `multicofork_π_one`, `multicofork_π_one_assoc`, `multicofork_π_three`, `multicofork_π_three_assoc`, `multicofork_π_zero`, `multicofork_π_zero_assoc`, `exists_desc`, `ι₀_desc`, `ι₀_desc_assoc`, `ι₁_desc`, `ι₁_desc_assoc`, `ι₃_desc`, `ι₃_desc_assoc`	35
Total	52

SSet.horn

Definitions

Name	Category	Theorems
`isColimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multicoequalizerDiagram` 📖	mathematical	—	`SSet.Subcomplex.MulticoequalizerDiagram` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `SSet.stdSimplex` `SSet.horn` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Set.instMembership` `Finset.instInsert`	—	`SSet.horn_eq_iSup` `SSet.stdSimplex.face_inter_face` `Finset.compl_insert` `Finset.ext`

SSet.horn₂₀

Definitions

Name	Category	Theorems
`ι₀₁` 📖	CompOp	1 math math: `isPushout`
`ι₀₂` 📖	CompOp	1 math math: `isPushout`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPushout` 📖	mathematical	—	`CategoryTheory.IsPushout` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `CategoryTheory.CosimplicialObject.δ` `ι₀₁` `ι₀₂`	—	`CategoryTheory.IsPushout.of_iso'` `Lattice.BicartSq.le₁₂` `sq` `Lattice.BicartSq.le₁₃` `Lattice.BicartSq.le₂₄` `Lattice.BicartSq.le₃₄` `SSet.Subcomplex.BicartSq.isPushout`
`sq` 📖	mathematical	—	`SSet.Subcomplex.BicartSq` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `SSet.stdSimplex` `SSet.stdSimplex.face` `Finset` `Finset.instSingleton` `Finset.instInsert` `SSet.horn`	—	`le_antisymm` `sup_le_iff` `SSet.face_le_horn` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `SSet.horn_eq_iSup` `iSup_le_iff` `Fintype.complete` `le_sup_right` `le_sup_left` `SSet.stdSimplex.face_inter_face` `Finset.inter_insert_of_mem` `Finset.inter_singleton_of_notMem` `Finset.instLawfulSingleton`

SSet.horn₂₁

Definitions

Name	Category	Theorems
`ι₀₁` 📖	CompOp	1 math math: `isPushout`
`ι₁₂` 📖	CompOp	1 math math: `isPushout`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPushout` 📖	mathematical	—	`CategoryTheory.IsPushout` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `CategoryTheory.CosimplicialObject.δ` `ι₀₁` `ι₁₂`	—	`CategoryTheory.IsPushout.of_iso'` `Lattice.BicartSq.le₁₂` `sq` `Lattice.BicartSq.le₁₃` `Lattice.BicartSq.le₂₄` `Lattice.BicartSq.le₃₄` `SSet.Subcomplex.BicartSq.isPushout`
`sq` 📖	mathematical	—	`SSet.Subcomplex.BicartSq` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `SSet.stdSimplex` `SSet.stdSimplex.face` `Finset` `Finset.instSingleton` `Finset.instInsert` `SSet.horn`	—	`le_antisymm` `sup_le_iff` `SSet.face_le_horn` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `SSet.horn_eq_iSup` `iSup_le_iff` `Fintype.complete` `le_sup_right` `le_sup_left` `SSet.stdSimplex.face_inter_face` `Finset.inter_insert_of_mem` `Finset.inter_singleton_of_notMem` `Finset.instLawfulSingleton`

SSet.horn₂₂

Definitions

Name	Category	Theorems
`ι₀₂` 📖	CompOp	1 math math: `isPushout`
`ι₁₂` 📖	CompOp	1 math math: `isPushout`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPushout` 📖	mathematical	—	`CategoryTheory.IsPushout` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `CategoryTheory.CosimplicialObject.δ` `ι₀₂` `ι₁₂`	—	`CategoryTheory.IsPushout.of_iso'` `Lattice.BicartSq.le₁₂` `sq` `Lattice.BicartSq.le₁₃` `Lattice.BicartSq.le₂₄` `Lattice.BicartSq.le₃₄` `SSet.Subcomplex.BicartSq.isPushout`
`sq` 📖	mathematical	—	`SSet.Subcomplex.BicartSq` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `CategoryTheory.Functor.category` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `SSet.stdSimplex` `SSet.stdSimplex.face` `Finset` `Finset.instSingleton` `Finset.instInsert` `SSet.horn`	—	`le_antisymm` `sup_le_iff` `SSet.face_le_horn` `SSet.horn_eq_iSup` `iSup_le_iff` `Fintype.complete` `le_sup_right` `le_sup_left` `SSet.stdSimplex.face_inter_face` `Finset.inter_insert_of_notMem` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Finset.inter_singleton_of_mem`

SSet.horn₃₁

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	6 math math: `ι₂_desc_assoc`, `ι₃_desc_assoc`, `ι₂_desc`, `ι₀_desc_assoc`, `ι₃_desc`, `ι₀_desc`
`ι₀` 📖	CompOp	3 math math: `exists_desc`, `ι₀_desc_assoc`, `ι₀_desc`
`ι₂` 📖	CompOp	3 math math: `exists_desc`, `ι₂_desc_assoc`, `ι₂_desc`
`ι₃` 📖	CompOp	3 math math: `exists_desc`, `ι₃_desc_assoc`, `ι₃_desc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`Quiver.Hom` `SSet` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet.Subcomplex.toSSet` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.horn` `CategoryTheory.CategoryStruct.comp` `ι₀` `ι₂` `ι₃`	—	`ι₀_desc` `ι₂_desc` `ι₃_desc`
`ι₀_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι₀` `desc`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Category.assoc` `SSet.horn.faceSingletonComplIso_inv_ι` `CategoryTheory.Limits.IsColimit.fac` `SSet.horn.multicoequalizerDiagram` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`ι₀_desc_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι₀` `desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₀_desc`
`ι₂_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι₂` `desc`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Category.assoc` `SSet.horn.faceSingletonComplIso_inv_ι` `CategoryTheory.Limits.IsColimit.fac` `SSet.horn.multicoequalizerDiagram`
`ι₂_desc_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι₂` `desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₂_desc`
`ι₃_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι₃` `desc`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Category.assoc` `SSet.horn.faceSingletonComplIso_inv_ι` `CategoryTheory.Limits.IsColimit.fac` `SSet.horn.multicoequalizerDiagram`
`ι₃_desc_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι₃` `desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₃_desc`

SSet.horn₃₁.desc

Definitions

Name	Category	Theorems
`multicofork` 📖	CompOp	7 math math: `multicofork_π_two`, `multicofork_pt`, `multicofork_π_two_assoc`, `multicofork_π_zero_assoc`, `multicofork_π_three_assoc`, `multicofork_π_zero`, `multicofork_π_three`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multicofork_pt` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingMultispan` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.WalkingMultispan.instSmallCategory` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanIndex.multispan` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `multicofork`	—	`SSet.horn.multicoequalizerDiagram`
`multicofork_π_three` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.Limits.Multicofork.π` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `multicofork` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `SSet.Subcomplex.toSSet` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso`	—	`SSet.horn.multicoequalizerDiagram`
`multicofork_π_three_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanIndex.right` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingMultispan` `CategoryTheory.Limits.WalkingMultispan.instSmallCategory` `CategoryTheory.Limits.MultispanIndex.multispan` `multicofork` `CategoryTheory.Limits.Multicofork.π` `SSet.Subcomplex.toSSet` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso`	—	`SSet.horn.multicoequalizerDiagram` `Mathlib.Tactic.Reassoc.eq_whisker'` `multicofork_π_three`
`multicofork_π_two` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.Limits.Multicofork.π` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `multicofork` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `SSet.Subcomplex.toSSet` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso`	—	`SSet.horn.multicoequalizerDiagram`
`multicofork_π_two_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanIndex.right` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingMultispan` `CategoryTheory.Limits.WalkingMultispan.instSmallCategory` `CategoryTheory.Limits.MultispanIndex.multispan` `multicofork` `CategoryTheory.Limits.Multicofork.π` `SSet.Subcomplex.toSSet` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso`	—	`SSet.horn.multicoequalizerDiagram` `Mathlib.Tactic.Reassoc.eq_whisker'` `multicofork_π_two`
`multicofork_π_zero` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.Limits.Multicofork.π` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `multicofork` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `SSet.Subcomplex.toSSet` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso`	—	`SSet.horn.multicoequalizerDiagram`
`multicofork_π_zero_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanIndex.right` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingMultispan` `CategoryTheory.Limits.WalkingMultispan.instSmallCategory` `CategoryTheory.Limits.MultispanIndex.multispan` `multicofork` `CategoryTheory.Limits.Multicofork.π` `SSet.Subcomplex.toSSet` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso`	—	`SSet.horn.multicoequalizerDiagram` `Mathlib.Tactic.Reassoc.eq_whisker'` `multicofork_π_zero`

SSet.horn₃₂

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	6 math math: `ι₁_desc`, `ι₃_desc`, `ι₀_desc`, `ι₁_desc_assoc`, `ι₃_desc_assoc`, `ι₀_desc_assoc`
`ι₀` 📖	CompOp	3 math math: `exists_desc`, `ι₀_desc`, `ι₀_desc_assoc`
`ι₁` 📖	CompOp	3 math math: `ι₁_desc`, `exists_desc`, `ι₁_desc_assoc`
`ι₃` 📖	CompOp	3 math math: `exists_desc`, `ι₃_desc`, `ι₃_desc_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`Quiver.Hom` `SSet` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `SSet.Subcomplex.toSSet` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.horn` `CategoryTheory.CategoryStruct.comp` `ι₀` `ι₁` `ι₃`	—	`ι₀_desc` `ι₁_desc` `ι₃_desc`
`ι₀_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι₀` `desc`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Category.assoc` `SSet.horn.faceSingletonComplIso_inv_ι` `CategoryTheory.Limits.IsColimit.fac` `SSet.horn.multicoequalizerDiagram`
`ι₀_desc_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι₀` `desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₀_desc`
`ι₁_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι₁` `desc`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Category.assoc` `SSet.horn.faceSingletonComplIso_inv_ι` `CategoryTheory.Limits.IsColimit.fac` `SSet.horn.multicoequalizerDiagram`
`ι₁_desc_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι₁` `desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₁_desc`
`ι₃_desc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι₃` `desc`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Category.assoc` `SSet.horn.faceSingletonComplIso_inv_ι` `CategoryTheory.Limits.IsColimit.fac` `SSet.horn.multicoequalizerDiagram`
`ι₃_desc_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `SSet.Subcomplex.toSSet` `SSet.horn` `ι₃` `desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι₃_desc`

SSet.horn₃₂.desc

Definitions

Name	Category	Theorems
`multicofork` 📖	CompOp	7 math math: `multicofork_π_one`, `multicofork_π_zero_assoc`, `multicofork_π_three`, `multicofork_pt`, `multicofork_π_zero`, `multicofork_π_three_assoc`, `multicofork_π_one_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multicofork_pt` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingMultispan` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.WalkingMultispan.instSmallCategory` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanIndex.multispan` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `multicofork`	—	`SSet.horn.multicoequalizerDiagram`
`multicofork_π_one` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.Limits.Multicofork.π` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `multicofork` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `SSet.Subcomplex.toSSet` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso`	—	`SSet.horn.multicoequalizerDiagram`
`multicofork_π_one_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanIndex.right` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingMultispan` `CategoryTheory.Limits.WalkingMultispan.instSmallCategory` `CategoryTheory.Limits.MultispanIndex.multispan` `multicofork` `CategoryTheory.Limits.Multicofork.π` `SSet.Subcomplex.toSSet` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso`	—	`SSet.horn.multicoequalizerDiagram` `Mathlib.Tactic.Reassoc.eq_whisker'` `multicofork_π_one`
`multicofork_π_three` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.Limits.Multicofork.π` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `multicofork` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `SSet.Subcomplex.toSSet` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso`	—	`SSet.horn.multicoequalizerDiagram`
`multicofork_π_three_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanIndex.right` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingMultispan` `CategoryTheory.Limits.WalkingMultispan.instSmallCategory` `CategoryTheory.Limits.MultispanIndex.multispan` `multicofork` `CategoryTheory.Limits.Multicofork.π` `SSet.Subcomplex.toSSet` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso`	—	`SSet.horn.multicoequalizerDiagram` `Mathlib.Tactic.Reassoc.eq_whisker'` `multicofork_π_three`
`multicofork_π_zero` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.Limits.Multicofork.π` `SSet` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `multicofork` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `SSet.Subcomplex.toSSet` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso`	—	`SSet.horn.multicoequalizerDiagram`
`multicofork_π_zero_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `CategoryTheory.CosimplicialObject.δ`	`CategoryTheory.CategoryStruct.comp` `SSet` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MultispanIndex.right` `CategoryTheory.Limits.MultispanShape.ofLinearOrder` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subtype.instLinearOrder` `Fin.instLinearOrder` `Set.instMembership` `CategoryTheory.Limits.MultispanIndex.map` `SSet.Subcomplex` `CategoryTheory.Functor.obj` `SSet.stdSimplex` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.instCompleteLatticeSubfunctor` `CategoryTheory.Limits.MultispanIndex.toLinearOrder` `CompleteLattice.MulticoequalizerDiagram.multispanIndex` `SSet.horn` `SSet.stdSimplex.face` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Fin.fintype` `Finset.instSingleton` `Finset.instInsert` `SSet.horn.multicoequalizerDiagram` `SSet.Subcomplex.toSSetFunctor` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingMultispan` `CategoryTheory.Limits.WalkingMultispan.instSmallCategory` `CategoryTheory.Limits.MultispanIndex.multispan` `multicofork` `CategoryTheory.Limits.Multicofork.π` `SSet.Subcomplex.toSSet` `CategoryTheory.Iso.inv` `SSet.stdSimplex.faceSingletonComplIso`	—	`SSet.horn.multicoequalizerDiagram` `Mathlib.Tactic.Reassoc.eq_whisker'` `multicofork_π_zero`

---

← Back to Index