BousfieldTransfiniteComposition

Statistics

Metric	Count
Definitions	0
Theorems `instIsStableUnderTransfiniteCompositionIsLocal`, `instIsStableUnderTransfiniteCompositionOfShapeIsLocal`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsStableUnderTransfiniteCompositionIsLocal` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition` `isLocal`	—	`instIsStableUnderTransfiniteCompositionOfShapeIsLocal`
`instIsStableUnderTransfiniteCompositionOfShapeIsLocal` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape` `isLocal`	—	`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` `Order.le_succ` `CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map_mem` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Category.id_comp` `PrincipalSeg.monotone` `CategoryTheory.TransfiniteCompositionOfShape.isWellOrderContinuous` `OrderHom.monotone` `CategoryTheory.Category.comp_id` `LT.lt.le` `CategoryTheory.Limits.IsColimit.fac` `CategoryTheory.TransfiniteCompositionOfShape.fac` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.WellOrderInductionData.sectionsMk_val_op_bot` `CategoryTheory.Iso.inv_hom_id_assoc`

---