Theorem CategoryTheory.IsPullback.of_horiz_isIso_mono

Modification history

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