Theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullback

Modification history

2025-10-03 22:56
Mathlib/CategoryTheory/MorphismProperty/Local.lean
feat(CategoryTheory/MorphismProperty): locality conditions (#30164) …
Added CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullbackView on Github →