Theorem CategoryTheory.Presieve.IsSeparatedFor.of_singleton_comp

Modification history

2026-08-12 15:35

Mathlib/CategoryTheory/Sites/IsSheafFor.lean

feat(CategoryTheory/Sites): criteria for `IsSheafFor` for a presieve generated by a single morphism (#42568)

Added CategoryTheory.Presieve.IsSeparatedFor.of_singleton_comp View on Github →