Theorem CategoryTheory.Sheaf.isSeparating

Modification history

2025-10-27 15:31

Mathlib/CategoryTheory/Generator/Sheaf.lean

refactor(CategoryTheory/Generator): use ObjectProperty instead of Set (#30269) …

Modified CategoryTheory.Sheaf.isSeparating View on Github →

2024-12-24 23:17

Mathlib/CategoryTheory/Generator/Sheaf.lean

feat(CategoryTheory/Sites): categories of sheaves have a separator (#19979) …

Added CategoryTheory.Sheaf.isSeparating View on Github →