Theorem CategoryTheory.classifier_isSheaf

Modification history

2026-03-20 18:13

Mathlib/CategoryTheory/Sites/Closed.lean

feat(CategoryTheory/Topos): Define subobject classifier for sheaf of types (#35867) …

Modified CategoryTheory.classifier_isSheaf View on Github →

2023-05-31 05:42

Mathlib/CategoryTheory/Sites/Closed.lean

feat: port CategoryTheory.Sites.Closed (#3356)

Added CategoryTheory.classifier_isSheaf View on Github →