Theorem CategoryTheory.Square.isPushout_iff_op_map_yoneda_isPullback

Modification history

2024-07-30 16:14
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Square.lean
feat(CategoryTheory): preservation of pullback/pushout squares (#15044) …
Added CategoryTheory.Square.isPushout_iff_op_map_yoneda_isPullbackView on Github →