Theorem CategoryTheory.MorphismProperty.of_zeroHypercover_target

Modification history

2026-06-18 23:59
Mathlib/CategoryTheory/MorphismProperty/Local.lean
chore: bump toolchain to v4.32.0-rc1 (#40732)
Added CategoryTheory.MorphismProperty.of_zeroHypercover_targetView on Github →
2026-05-29 00:22
Mathlib/CategoryTheory/MorphismProperty/Local.lean
refactor(CategoryTheory): redefine `MorphismProperty.IsLocalAtTarget` in terms of presieves (#39978) …
Deleted CategoryTheory.MorphismProperty.of_zeroHypercover_targetView on Github →
2025-10-13 13:57
Mathlib/CategoryTheory/MorphismProperty/Local.lean
feat(CategoryTheory/Sites): small `0`-hypercovers (#30321) …
Added CategoryTheory.MorphismProperty.of_zeroHypercover_targetView on Github →