Theorem CategoryTheory.Limits.closedUnderLimitsOfShape_walkingParallelPair_isIndObject

Modification history

2025-10-27 09:15
Mathlib/CategoryTheory/Limits/Indization/Equalizers.lean
refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape (#29881) …
Deleted CategoryTheory.Limits.closedUnderLimitsOfShape_walkingParallelPair_isIndObjectView on Github →
2025-01-28 09:37
Mathlib/CategoryTheory/Limits/Indization/Equalizers.lean
feat: equalizers and coequalizers in the category of ind-objects (#21139) …
Added CategoryTheory.Limits.closedUnderLimitsOfShape_walkingParallelPair_isIndObjectView on Github →