mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(CategoryTheory): add some instances for essentially small sites

Open dagurtomas opened this issue 1 year ago • 10 comments

This PR proves that the properties PreservesSheafification and WEqualsLocallyBijective hold for an essentially small site if they hold for an equivalent small site.

Open in Gitpod

dagurtomas avatar Jun 03 '24 21:06 dagurtomas