Theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover

Modification history

2026-05-29 00:22

Mathlib/CategoryTheory/MorphismProperty/Local.lean

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

Modified CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover View on Github →

2025-10-03 22:56

Mathlib/CategoryTheory/MorphismProperty/Local.lean

feat(CategoryTheory/MorphismProperty): locality conditions (#30164) …

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