Theorem CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_apply

Modification history

2026-04-14 15:27
Mathlib/CategoryTheory/Limits/ColimitLimit.lean
refactor(CategoryTheory): one-field structure morphisms in the category of types (#36613) …
Deleted CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_applyView on Github →
2024-03-26 07:43
Mathlib/CategoryTheory/Limits/ColimitLimit.lean
refactor: generalize universes for commuting filtered colimits and finite limits (#11325)
Modified CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_applyView on Github →
2023-03-13 13:46
Mathlib/CategoryTheory/Limits/ColimitLimit.lean
feat: port CategoryTheory.Limits.ColimitLimit (#2810)
Added CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_applyView on Github →