Documentation Verification Report

TransfiniteComposition

📁 Source: Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean

Statistics

Metric	Count
Definitions `IsStableUnderInfiniteComposition`, `IsStableUnderTransfiniteComposition`, `IsStableUnderTransfiniteCompositionOfShape`, `ici`, `id`, `iic`, `map`, `ofArrowIso`, `ofComp`, `ofComposableArrows`, `ofLE`, `ofMem`, `ofOrderIso`, `toTransfiniteCompositionOfShape`, `transfiniteCompositions`, `transfiniteCompositionsOfShape`	16
Theorems `instIsMultiplicative`, `instOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits`, `isStableUnderTransfiniteCompositionOfShape`, `shrink`, `shrink₀`, `le`, `of_isStableUnderColimitsOfShape`, `mem`, `mem_map_bot_le`, `instIsIsoAppIncl`, `instIsIsoMapF`, `isIso`, `map_mem`, `map_toTransfiniteCompositionOfShape`, `mem`, `mem_incl_app`, `mem_map`, `ofArrowIso_toTransfiniteCompositionOfShape`, `ofComposableArrows_F`, `ofComposableArrows_incl_app`, `ofComposableArrows_isColimit_desc`, `ofComposableArrows_isoBot_hom`, `ofComposableArrows_isoBot_inv`, `ofLE_toTransfiniteCompositionOfShape`, `instIsStableUnderTransfiniteCompositionOfShapeOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits`, `instRespectsIsoTransfiniteCompositionsOfShape`, `isStableUnderTransfiniteCompositionOfShape_iff`, `isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso`, `le_transfiniteCompositions`, `transfiniteCompositionsOfShape_eq_of_orderIso`, `transfiniteCompositionsOfShape_le`, `transfiniteCompositionsOfShape_le_transfiniteCompositions`, `transfiniteCompositionsOfShape_map_of_preserves`, `transfiniteCompositionsOfShape_monotone`, `transfiniteCompositions_iff`, `transfiniteCompositions_le`, `transfiniteCompositions_le_iff`, `transfiniteCompositions_monotone`	38
Total	54

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`IsStableUnderInfiniteComposition` 📖	MathDef	—
`IsStableUnderTransfiniteComposition` 📖	CompData	5 math math: `IsStableUnderTransfiniteComposition.shrink₀`, `CategoryTheory.IsGrothendieckAbelian.instIsStableUnderTransfiniteCompositionMonomorphisms`, `CategoryTheory.ObjectProperty.instIsStableUnderTransfiniteCompositionIsLocal`, `IsStableUnderTransfiniteComposition.instOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits`, `IsStableUnderTransfiniteComposition.shrink`
`IsStableUnderTransfiniteCompositionOfShape` 📖	CompData	9 math math: `instIsStableUnderTransfiniteCompositionOfShapeFunctorMonomorphismsOfHasPullbacksOfHasIterationOfShape`, `instIsStableUnderTransfiniteCompositionOfShapeFunctorFunctorCategoryOfHasIterationOfShape`, `instIsStableUnderTransfiniteCompositionOfShapeOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits`, `isStableUnderTransfiniteCompositionOfShape_llp`, `isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso`, `IsStableUnderTransfiniteCompositionOfShape.of_isStableUnderColimitsOfShape`, `CategoryTheory.ObjectProperty.instIsStableUnderTransfiniteCompositionOfShapeIsLocal`, `isStableUnderTransfiniteCompositionOfShape_iff`, `IsStableUnderTransfiniteComposition.isStableUnderTransfiniteCompositionOfShape`
`transfiniteCompositions` 📖	CompOp	11 math math: `transfiniteCompositionsOfShape_le_transfiniteCompositions`, `llp_rlp_of_hasSmallObjectArgument`, `retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp`, `CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument`, `transfiniteCompositions_le`, `transfiniteCompositions_pushouts_coproducts_le_llp_rlp`, `transfiniteCompositions_iff`, `transfiniteCompositions_monotone`, `transfiniteCompositions_le_llp_rlp`, `le_transfiniteCompositions`, `transfiniteCompositions_le_iff`
`transfiniteCompositionsOfShape` 📖	CompOp	16 math math: `transfiniteCompositionsOfShape_eq_of_orderIso`, `TransfiniteCompositionOfShape.mem`, `transfiniteCompositionsOfShape_le_transfiniteCompositions`, `transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp`, `transfiniteCompositionsOfShape_le`, `transfiniteCompositionsOfShape_monotone`, `IsStableUnderTransfiniteCompositionOfShape.le`, `instRespectsIsoTransfiniteCompositionsOfShape`, `transfiniteCompositionsOfShape_le_llp_rlp`, `llp_rlp_of_hasSmallObjectArgument'`, `retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp`, `isStableUnderTransfiniteCompositionOfShape_iff`, `CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument'`, `CategoryTheory.SmallObject.transfiniteCompositionsOfShape_ιObj`, `transfiniteCompositions_iff`, `transfiniteCompositionsOfShape_map_of_preserves`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsStableUnderTransfiniteCompositionOfShapeOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits` 📖	mathematical	—	`IsStableUnderTransfiniteCompositionOfShape`	—	`IsStableUnderTransfiniteCompositionOfShape.of_isStableUnderColimitsOfShape` `IsStableUnderFilteredColimits.isStableUnderColimitsOfShape` `CategoryTheory.isFiltered_of_directed_le_nonempty` `SemilatticeSup.instIsDirectedOrder` `bot_nonempty`
`instRespectsIsoTransfiniteCompositionsOfShape` 📖	mathematical	—	`RespectsIso` `transfiniteCompositionsOfShape`	—	`RespectsIso.of_respects_arrow_iso`
`isStableUnderTransfiniteCompositionOfShape_iff` 📖	mathematical	—	`IsStableUnderTransfiniteCompositionOfShape` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `transfiniteCompositionsOfShape`	—	—
`isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso` 📖	mathematical	—	`IsStableUnderTransfiniteCompositionOfShape`	—	`transfiniteCompositionsOfShape_eq_of_orderIso`
`le_transfiniteCompositions` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `transfiniteCompositions`	—	`le_trans` `UnivLE.small` `univLE_of_max` `UnivLE.self` `instWellFoundedLTShrink` `IsWellOrder.toIsWellFounded` `Fin.Lt.isWellOrder` `TransfiniteCompositionOfShape.mem` `transfiniteCompositionsOfShape_le_transfiniteCompositions`
`transfiniteCompositionsOfShape_eq_of_orderIso` 📖	mathematical	—	`transfiniteCompositionsOfShape`	—	`ext`
`transfiniteCompositionsOfShape_le` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `transfiniteCompositionsOfShape`	—	`IsStableUnderTransfiniteCompositionOfShape.le`
`transfiniteCompositionsOfShape_le_transfiniteCompositions` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `transfiniteCompositionsOfShape` `transfiniteCompositions`	—	`transfiniteCompositions_iff`
`transfiniteCompositionsOfShape_map_of_preserves` 📖	mathematical	—	`transfiniteCompositionsOfShape` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`TransfiniteCompositionOfShape.mem`
`transfiniteCompositionsOfShape_monotone` 📖	mathematical	—	`Monotone` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `transfiniteCompositionsOfShape`	—	—
`transfiniteCompositions_iff` 📖	mathematical	—	`transfiniteCompositions` `transfiniteCompositionsOfShape`	—	—
`transfiniteCompositions_le` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `transfiniteCompositions`	—	`transfiniteCompositions_iff` `transfiniteCompositionsOfShape_le` `IsStableUnderTransfiniteComposition.isStableUnderTransfiniteCompositionOfShape`
`transfiniteCompositions_le_iff` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `transfiniteCompositions`	—	`LE.le.trans` `le_transfiniteCompositions` `transfiniteCompositions_monotone` `transfiniteCompositions_le`
`transfiniteCompositions_monotone` 📖	mathematical	—	`Monotone` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `transfiniteCompositions`	—	`transfiniteCompositions_iff` `transfiniteCompositionsOfShape_le_transfiniteCompositions` `transfiniteCompositionsOfShape_monotone`

CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsMultiplicative` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative`	—	`CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le` `IsWellOrder.toIsWellFounded` `Fin.Lt.isWellOrder` `isStableUnderTransfiniteCompositionOfShape` `shrink₀` `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem`
`instOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition`	—	`CategoryTheory.MorphismProperty.instIsStableUnderTransfiniteCompositionOfShapeOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits`
`isStableUnderTransfiniteCompositionOfShape` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape`	—	—
`shrink` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition`	—	`UnivLE.small` `instWellFoundedLTShrink` `CategoryTheory.MorphismProperty.isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso` `isStableUnderTransfiniteCompositionOfShape`
`shrink₀` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition`	—	`shrink` `univLE_of_max` `UnivLE.self`

CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape`	—	—
`of_isStableUnderColimitsOfShape` 📖	mathematical	`CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape`	—	`of_isStableUnderColimitsOfShape.mem`

CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.of_isStableUnderColimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem` 📖	—	`CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.TransfiniteCompositionOfShape.fac` `CategoryTheory.Category.comp_id` `CategoryTheory.MorphismProperty.colimitsOfShape_le` `CategoryTheory.MorphismProperty.colimitsOfShape.of_isColimit` `mem_map_bot_le` `bot_le`
`mem_map_bot_le` 📖	mathematical	`CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.Functor.obj` `CategoryTheory.TransfiniteCompositionOfShape.F` `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `CategoryTheory.Functor.map`	—	`bot_le` `CategoryTheory.Functor.map_id` `CategoryTheory.MorphismProperty.id_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities` `IsMin.eq_bot` `Order.le_succ` `LE.le.trans` `CategoryTheory.homOfLE_comp` `CategoryTheory.Functor.map_comp` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map_mem` `CategoryTheory.MorphismProperty.colimitsOfShape_le` `Set.ordConnected_Iio` `Order.IsSuccLimit.bot_lt` `Subtype.wellFoundedLT` `CategoryTheory.MorphismProperty.colimitsOfShape.of_isColimit` `PrincipalSeg.monotone` `CategoryTheory.TransfiniteCompositionOfShape.isWellOrderContinuous`

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape

Definitions

Name	Category	Theorems
`ici` 📖	CompOp	—
`id` 📖	CompOp	—
`iic` 📖	CompOp	—
`map` 📖	CompOp	1 math math: `map_toTransfiniteCompositionOfShape`
`ofArrowIso` 📖	CompOp	1 math math: `ofArrowIso_toTransfiniteCompositionOfShape`
`ofComp` 📖	CompOp	—
`ofComposableArrows` 📖	CompOp	5 math math: `ofComposableArrows_incl_app`, `ofComposableArrows_isColimit_desc`, `ofComposableArrows_F`, `ofComposableArrows_isoBot_inv`, `ofComposableArrows_isoBot_hom`
`ofLE` 📖	CompOp	1 math math: `ofLE_toTransfiniteCompositionOfShape`
`ofMem` 📖	CompOp	—
`ofOrderIso` 📖	CompOp	—
`toTransfiniteCompositionOfShape` 📖	CompOp	22 math math: `ofComposableArrows_incl_app`, `ofComposableArrows_isColimit_desc`, `instIsIsoAppIncl`, `CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_isoBot`, `ofLE_toTransfiniteCompositionOfShape`, `instIsIsoMapF`, `ofComposableArrows_F`, `CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.of_isStableUnderColimitsOfShape.mem_map_bot_le`, `CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_incl`, `ofArrowIso_toTransfiniteCompositionOfShape`, `ofComposableArrows_isoBot_inv`, `map_mem`, `CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_F`, `CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right`, `CategoryTheory.SmallObject.transfiniteCompositionOfShapeSuccStructPropιIteration_F`, `map_toTransfiniteCompositionOfShape`, `CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right_assoc`, `ofComposableArrows_isoBot_hom`, `HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape_toTransfiniteCompositionOfShape`, `mem_map`, `CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_isColimit`, `mem_incl_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIsoAppIncl` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.TransfiniteCompositionOfShape.F` `toTransfiniteCompositionOfShape` `CategoryTheory.MorphismProperty.isomorphisms` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.NatTrans.app` `CategoryTheory.TransfiniteCompositionOfShape.incl`	—	`mem_incl_app` `CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.instOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits` `CategoryTheory.MorphismProperty.IsMultiplicative.instIsomorphisms` `CategoryTheory.MorphismProperty.RespectsIso.isomorphisms` `CategoryTheory.MorphismProperty.instIsStableUnderFilteredColimitsIsomorphisms`
`instIsIsoMapF` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.TransfiniteCompositionOfShape.F` `toTransfiniteCompositionOfShape` `CategoryTheory.MorphismProperty.isomorphisms` `CategoryTheory.Functor.map`	—	`mem_map` `CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.instOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits` `CategoryTheory.MorphismProperty.IsMultiplicative.instIsomorphisms` `CategoryTheory.MorphismProperty.RespectsIso.isomorphisms` `CategoryTheory.MorphismProperty.instIsStableUnderFilteredColimitsIsomorphisms`
`isIso` 📖	mathematical	—	`CategoryTheory.IsIso`	—	`CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le` `CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.isStableUnderTransfiniteCompositionOfShape` `CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.instOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits` `CategoryTheory.MorphismProperty.IsMultiplicative.instIsomorphisms` `CategoryTheory.MorphismProperty.RespectsIso.isomorphisms` `CategoryTheory.MorphismProperty.instIsStableUnderFilteredColimitsIsomorphisms` `mem`
`map_mem` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `CategoryTheory.TransfiniteCompositionOfShape.F` `toTransfiniteCompositionOfShape` `Order.succ` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Order.le_succ`	—	—
`map_toTransfiniteCompositionOfShape` 📖	mathematical	—	`toTransfiniteCompositionOfShape` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `map` `CategoryTheory.TransfiniteCompositionOfShape.map` `CategoryTheory.MorphismProperty.inverseImage`	—	—
`mem` 📖	mathematical	—	`CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape`	—	—
`mem_incl_app` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.TransfiniteCompositionOfShape.F` `toTransfiniteCompositionOfShape` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.NatTrans.app` `CategoryTheory.TransfiniteCompositionOfShape.incl`	—	`CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le` `Set.ordConnected_Ici` `Subtype.wellFoundedLT` `CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.isStableUnderTransfiniteCompositionOfShape` `mem`
`mem_map` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.TransfiniteCompositionOfShape.F` `toTransfiniteCompositionOfShape` `CategoryTheory.Functor.map`	—	`CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le` `CategoryTheory.leOfHom` `Set.ordConnected_Ici` `Set.ordConnected_Iic` `Subtype.wellFoundedLT` `CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.isStableUnderTransfiniteCompositionOfShape` `mem` `bot_le`
`ofArrowIso_toTransfiniteCompositionOfShape` 📖	mathematical	—	`toTransfiniteCompositionOfShape` `ofArrowIso` `CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso`	—	—
`ofComposableArrows_F` 📖	mathematical	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Fin.castSucc_le_succ`	`CategoryTheory.TransfiniteCompositionOfShape.F` `Fin.instLinearOrder` `HeytingAlgebra.toOrderBot` `Fin.instHeytingAlgebra` `CategoryTheory.ComposableArrows.left` `CategoryTheory.ComposableArrows.right` `CategoryTheory.ComposableArrows.hom` `Fin.instSuccOrder` `IsWellOrder.toIsWellFounded` `Preorder.toLT` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Fin.Lt.isWellOrder` `toTransfiniteCompositionOfShape` `ofComposableArrows`	—	`Fin.castSucc_le_succ` `IsWellOrder.toIsWellFounded` `Fin.Lt.isWellOrder`
`ofComposableArrows_incl_app` 📖	mathematical	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Fin.castSucc_le_succ`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.TransfiniteCompositionOfShape.incl` `Fin.instLinearOrder` `HeytingAlgebra.toOrderBot` `Fin.instHeytingAlgebra` `CategoryTheory.ComposableArrows.left` `CategoryTheory.ComposableArrows.right` `CategoryTheory.ComposableArrows.hom` `Fin.instSuccOrder` `IsWellOrder.toIsWellFounded` `Preorder.toLT` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Fin.Lt.isWellOrder` `toTransfiniteCompositionOfShape` `ofComposableArrows` `CategoryTheory.Limits.IsTerminal.from` `Fin.isTerminalLast`	—	`Fin.castSucc_le_succ` `IsWellOrder.toIsWellFounded` `Fin.Lt.isWellOrder`
`ofComposableArrows_isColimit_desc` 📖	mathematical	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Fin.castSucc_le_succ`	`CategoryTheory.Limits.IsColimit.desc` `CategoryTheory.Limits.coconeOfDiagramTerminal` `Fin.isTerminalLast` `CategoryTheory.TransfiniteCompositionOfShape.isColimit` `Fin.instLinearOrder` `HeytingAlgebra.toOrderBot` `Fin.instHeytingAlgebra` `CategoryTheory.ComposableArrows.left` `CategoryTheory.ComposableArrows.right` `CategoryTheory.ComposableArrows.hom` `Fin.instSuccOrder` `IsWellOrder.toIsWellFounded` `Preorder.toLT` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Fin.Lt.isWellOrder` `toTransfiniteCompositionOfShape` `ofComposableArrows` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.Cocone.ι`	—	`Fin.castSucc_le_succ` `IsWellOrder.toIsWellFounded` `Fin.Lt.isWellOrder`
`ofComposableArrows_isoBot_hom` 📖	mathematical	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Fin.castSucc_le_succ`	`CategoryTheory.Iso.hom` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Fin.instLinearOrder` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `HeytingAlgebra.toOrderBot` `Fin.instHeytingAlgebra` `CategoryTheory.TransfiniteCompositionOfShape.isoBot` `CategoryTheory.ComposableArrows.left` `CategoryTheory.ComposableArrows.right` `CategoryTheory.ComposableArrows.hom` `Fin.instSuccOrder` `IsWellOrder.toIsWellFounded` `Preorder.toLT` `Fin.Lt.isWellOrder` `toTransfiniteCompositionOfShape` `ofComposableArrows` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`Fin.castSucc_le_succ` `IsWellOrder.toIsWellFounded` `Fin.Lt.isWellOrder`
`ofComposableArrows_isoBot_inv` 📖	mathematical	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.Functor.map` `CategoryTheory.homOfLE` `Fin.castSucc_le_succ`	`CategoryTheory.Iso.inv` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Fin.instLinearOrder` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `HeytingAlgebra.toOrderBot` `Fin.instHeytingAlgebra` `CategoryTheory.TransfiniteCompositionOfShape.isoBot` `CategoryTheory.ComposableArrows.left` `CategoryTheory.ComposableArrows.right` `CategoryTheory.ComposableArrows.hom` `Fin.instSuccOrder` `IsWellOrder.toIsWellFounded` `Preorder.toLT` `Fin.Lt.isWellOrder` `toTransfiniteCompositionOfShape` `ofComposableArrows` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`Fin.castSucc_le_succ` `IsWellOrder.toIsWellFounded` `Fin.Lt.isWellOrder`
`ofLE_toTransfiniteCompositionOfShape` 📖	mathematical	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	`toTransfiniteCompositionOfShape` `ofLE`	—	—

---

← Back to Index