Theorem CategoryTheory.isSheaf_iff_equalizerCondition

Modification history

2023-11-21 07:27
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
chore(CategoryTheory): relax assumptions on category for regular sheaf condition (#8514) …
Deleted CategoryTheory.isSheaf_iff_equalizerConditionView on Github →
2023-10-20 14:35
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
feat: description of sheaves for regular sieves (#6919) …
Added CategoryTheory.isSheaf_iff_equalizerConditionView on Github →