Theorem CategoryTheory.Presieve.singleton_le_iff

Modification history

2026-08-23 14:46

Mathlib/CategoryTheory/Sites/Sieves.lean

refactor(CategoryTheory/Sites): split long file Sieves.lean (#43014) …

Modified CategoryTheory.Presieve.singleton_le_iff View on Github →

2026-08-12 15:35

Mathlib/CategoryTheory/Sites/Sieves.lean

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

Added CategoryTheory.Presieve.singleton_le_iff View on Github →