Def CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso

Modification history

2025-02-08 20:24

Mathlib/CategoryTheory/Limits/Shapes/Preorder/TransfiniteCompositionOfShape.lean

refactor(CategoryTheory): a structure describing transfinite compositions (#21417) …

Added CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso View on Github →