Theorem CategoryTheory.Limits.IsIPCOfShape.of_forall_exists

Modification history

2026-05-06 00:44

Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean

refactor(CategoryTheory/Limits): redefine `IsIPC` in terms of `IsIPCOfShape` (#38378) …

Added CategoryTheory.Limits.IsIPCOfShape.of_forall_exists View on Github →