Theorem CategoryTheory.Sheaf.Subcanonical.isSheaf_of_representable

Modification history

2024-10-04 10:12
Mathlib/CategoryTheory/Sites/Canonical.lean
refactor(CategoryTheory): generalize universes for representable functors (#17389) …
Deleted CategoryTheory.Sheaf.Subcanonical.isSheaf_of_representableView on Github →
2023-06-05 13:56
Mathlib/CategoryTheory/Sites/Canonical.lean
feat: port CategoryTheory.Sites.Canonical (#3936)
Added CategoryTheory.Sheaf.Subcanonical.isSheaf_of_representableView on Github →