Theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.of_zeroHypercover

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.of_zeroHypercover View on Github →