Theorem CategoryTheory.Limits.hasIterationOfShape_of_initialSeg

Modification history

2025-02-02 20:52
Mathlib/CategoryTheory/Limits/Shapes/Preorder/HasIterationOfShape.lean
feat(CategoryTheory/Limits/Shapes/Preorder): principal segments (#21055) …
Added CategoryTheory.Limits.hasIterationOfShape_of_initialSegView on Github →