mathlib

9ceb3c2a - feat(topology/sheaf_condition): connect sheaves on sites and on spaces without has_products (#11706)

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. - [x] depends on: #11692 Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>