Theorem CategoryTheory.IsPushout.of_horiz_isIso_epi

Modification history

2025-07-15 08:52
Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
feat(CategoryTheory/Topos): subobject classifier without limits (#26556) …
Added CategoryTheory.IsPushout.of_horiz_isIso_epiView on Github →