Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-07 19:33 9ceb3c2a

View on Github →

feat(topology/sheaf_condition): connect sheaves on sites and on spaces without has_products (#11706) As an application of #11692, show that the is_sheaf_opens_le_cover sheaf condition on spaces is equivalent to is_sheaf on sites, thereby connecting sheaves on sites and on spaces without the value category has_products for the first time. (@justus-springer: you might want to take a look so as to determine whether and which of your work in #9609 should be deprecated.) This could be seen as a step towards refactoring sheaves on spaces through sheaves on sites.

Estimated changes