Documentation Verification Report

Basic

📁 Source: Mathlib/AlgebraicTopology/RelativeCellComplex/Basic.lean

Statistics

Metric	Count
Definitions `RelativeCellComplex`, `Cells`, `i`, `j`, `k`, `ι`, `attachCells`, `toTransfiniteCompositionOfShape`, `transfiniteCompositionOfShape`	9
Theorems `hj`, `hom_ext`, `transfiniteCompositionOfShape_toTransfiniteCompositionOfShape`	3
Total	12

HomotopicalAlgebra

Definitions

Name	Category	Theorems
`RelativeCellComplex` 📖	CompData	—

HomotopicalAlgebra.RelativeCellComplex

Definitions

Name	Category	Theorems
`Cells` 📖	CompData	—
`attachCells` 📖	CompOp	—
`toTransfiniteCompositionOfShape` 📖	CompOp	5 math math: `CategoryTheory.SmallObject.ιFunctorObj_eq`, `CategoryTheory.SmallObject.πFunctorObj_eq`, `CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.preservesColimit`, `CategoryTheory.SmallObject.preservesColimit`, `transfiniteCompositionOfShape_toTransfiniteCompositionOfShape`
`transfiniteCompositionOfShape` 📖	CompOp	1 math math: `transfiniteCompositionOfShape_toTransfiniteCompositionOfShape`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Cells.j` `Cells.i` `Cells.ι`	—	—	`CategoryTheory.Limits.IsColimit.hom_ext` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.TransfiniteCompositionOfShape.fac_assoc` `IsMin.eq_bot` `HomotopicalAlgebra.AttachCells.hom_ext` `Order.le_succ` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Category.id_comp` `Cells.hj` `CategoryTheory.Category.assoc` `PrincipalSeg.monotone` `CategoryTheory.TransfiniteCompositionOfShape.isWellOrderContinuous`
`transfiniteCompositionOfShape_toTransfiniteCompositionOfShape` 📖	mathematical	—	`CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape` `CategoryTheory.MorphismProperty.pushouts` `CategoryTheory.MorphismProperty.coproducts` `CategoryTheory.MorphismProperty.ofHoms` `transfiniteCompositionOfShape` `toTransfiniteCompositionOfShape`	—	—

HomotopicalAlgebra.RelativeCellComplex.Cells

Definitions

Name	Category	Theorems
`i` 📖	CompOp	—
`j` 📖	CompOp	1 math math: `hj`
`k` 📖	CompOp	—
`ι` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hj` 📖	mathematical	—	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `j`	—	—

---

← Back to Index