Theorem CategoryTheory.equalizerCondition_of_regular

Modification history

2023-11-21 08:44
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
feat(CategoryTheory): the regular topology is subcanonical (#8529) …
Deleted CategoryTheory.equalizerCondition_of_regularView on Github →
2023-11-17 00:15
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
refactor(CategoryTheory): simplify the proof of the characterisation of regular sheaves using the new arrows API (#8443)
Added CategoryTheory.equalizerCondition_of_regularView on Github →