Documentation Verification Report

TransfiniteIteration

📁 Source: Mathlib/CategoryTheory/SmallObject/TransfiniteIteration.lean

Statistics

Metric	Count
Definitions `isColimitIterationCocone`, `iter`, `iteration`, `iterationCocone`, `iterationFunctor`, `iterationFunctorObjBotIso`, `iterationFunctorObjSuccIso`, `transfiniteCompositionOfShapeιIteration`, `ιIteration`, `ιIterationFunctor`	10
Theorems `arrowMk_iterationFunctor_map`, `instIsWellOrderContinuousIterationFunctor`, `iterationCocone_pt`, `iterationFunctor_map_succ`, `iterationFunctor_map_succ_assoc`, `iterationFunctor_obj`, `prop_iterationFunctor_map_succ`, `transfiniteCompositionOfShapeιIteration_F`, `transfiniteCompositionOfShapeιIteration_incl`, `transfiniteCompositionOfShapeιIteration_isColimit`, `transfiniteCompositionOfShapeιIteration_isoBot`	11
Total	21

CategoryTheory.SmallObject.SuccStruct

Definitions

Name	Category	Theorems
`isColimitIterationCocone` 📖	CompOp	1 math math: `transfiniteCompositionOfShapeιIteration_isColimit`
`iter` 📖	CompOp	—
`iteration` 📖	CompOp	5 math math: `transfiniteCompositionOfShapeιIteration_isoBot`, `transfiniteCompositionOfShapeιIteration_incl`, `transfiniteCompositionOfShapeιIteration_F`, `iterationCocone_pt`, `transfiniteCompositionOfShapeιIteration_isColimit`
`iterationCocone` 📖	CompOp	2 math math: `transfiniteCompositionOfShapeιIteration_incl`, `iterationCocone_pt`
`iterationFunctor` 📖	CompOp	9 math math: `arrowMk_iterationFunctor_map`, `iterationFunctor_map_succ_assoc`, `iterationFunctor_map_succ`, `transfiniteCompositionOfShapeιIteration_incl`, `prop_iterationFunctor_map_succ`, `transfiniteCompositionOfShapeιIteration_F`, `iterationCocone_pt`, `instIsWellOrderContinuousIterationFunctor`, `iterationFunctor_obj`
`iterationFunctorObjBotIso` 📖	CompOp	1 math math: `transfiniteCompositionOfShapeιIteration_isoBot`
`iterationFunctorObjSuccIso` 📖	CompOp	2 math math: `iterationFunctor_map_succ_assoc`, `iterationFunctor_map_succ`
`transfiniteCompositionOfShapeιIteration` 📖	CompOp	4 math math: `transfiniteCompositionOfShapeιIteration_isoBot`, `transfiniteCompositionOfShapeιIteration_incl`, `transfiniteCompositionOfShapeιIteration_F`, `transfiniteCompositionOfShapeιIteration_isColimit`
`ιIteration` 📖	CompOp	4 math math: `transfiniteCompositionOfShapeιIteration_isoBot`, `transfiniteCompositionOfShapeιIteration_incl`, `transfiniteCompositionOfShapeιIteration_F`, `transfiniteCompositionOfShapeιIteration_isColimit`
`ιIterationFunctor` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arrowMk_iterationFunctor_map` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `iterationFunctor` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Set.Elem` `Set.Iic` `Subtype.preorder` `Set` `Set.instMembership` `Iteration.F` `LE.le.trans`	—	`LE.le.trans` `Iteration.arrow_mk_mapObj` `CategoryTheory.Arrow.ext` `Iteration.congr_obj` `Iteration.congr_map`
`instIsWellOrderContinuousIterationFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsWellOrderContinuous` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `iterationFunctor`	—	`PrincipalSeg.monotone` `iterationFunctor_obj` `CategoryTheory.Arrow.mk_injective` `LE.le.trans` `LT.lt.le` `CategoryTheory.Arrow.arrow_mk_comp_eqToHom` `CategoryTheory.Arrow.arrow_mk_eqToHom_comp` `arrowMk_iterationFunctor_map` `CategoryTheory.leOfHom` `CategoryTheory.Category.comp_id`
`iterationCocone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `iterationFunctor` `iterationCocone` `iteration`	—	—
`iterationFunctor_map_succ` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.Functor.map` `Preorder.smallCategory` `iterationFunctor` `Order.succ` `CategoryTheory.homOfLE` `Order.le_succ` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `succ` `toSucc` `CategoryTheory.Iso.inv` `iterationFunctorObjSuccIso`	—	`prop.fac` `Order.le_succ` `prop_iterationFunctor_map_succ`
`iterationFunctor_map_succ_assoc` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `iterationFunctor` `Order.succ` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Order.le_succ` `succ` `toSucc` `CategoryTheory.Iso.inv` `iterationFunctorObjSuccIso`	—	`Order.le_succ` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iterationFunctor_map_succ`
`iterationFunctor_obj` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `iterationFunctor` `Set.Elem` `Set.Iic` `Subtype.preorder` `Set` `Set.instMembership` `Iteration.F`	—	`Iteration.congr_obj`
`prop_iterationFunctor_map_succ` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`prop` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `iterationFunctor` `Order.succ` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Order.le_succ`	—	`CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map_mem`
`transfiniteCompositionOfShapeιIteration_F` 📖	mathematical	—	`CategoryTheory.TransfiniteCompositionOfShape.F` `X₀` `iteration` `ιIteration` `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape` `prop` `transfiniteCompositionOfShapeιIteration` `iterationFunctor`	—	—
`transfiniteCompositionOfShapeιIteration_incl` 📖	mathematical	—	`CategoryTheory.TransfiniteCompositionOfShape.incl` `X₀` `iteration` `ιIteration` `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape` `prop` `transfiniteCompositionOfShapeιIteration` `CategoryTheory.Limits.Cocone.ι` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `iterationFunctor` `iterationCocone`	—	—
`transfiniteCompositionOfShapeιIteration_isColimit` 📖	mathematical	—	`CategoryTheory.TransfiniteCompositionOfShape.isColimit` `X₀` `iteration` `ιIteration` `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape` `prop` `transfiniteCompositionOfShapeιIteration` `isColimitIterationCocone`	—	—
`transfiniteCompositionOfShapeιIteration_isoBot` 📖	mathematical	—	`CategoryTheory.TransfiniteCompositionOfShape.isoBot` `X₀` `iteration` `ιIteration` `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape` `prop` `transfiniteCompositionOfShapeιIteration` `iterationFunctorObjBotIso`	—	—

---

← Back to Index