Theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_small

Modification history

2026-05-29 00:22

Mathlib/CategoryTheory/MorphismProperty/Local.lean

refactor(CategoryTheory): redefine `MorphismProperty.IsLocalAtTarget` in terms of presieves (#39978) …

Added CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_small View on Github →