mathlib3

58d0bfcc - feat(topology/sheaves): alternate formulation of the sheaf condition (#4190)

feat(topology/sheaves): alternate formulation of the sheaf condition (#4190) Currently the sheaf condition is stated as it often is in textbooks, e.g. https://stacks.math.columbia.edu/tag/0072. That is, it is about an equalizer of the two maps `∏ F.obj (U i) ⟶ ∏ F.obj (U i) ⊓ (U j)`. This PR adds an equivalent formulation, saying that `F.obj (supr U)` (with its natural projection maps) is the limit of the diagram consisting of the `F.obj (U i)` and the `F.obj (U i ⊓ U j)`. I'd like to add further reformulations in subsequent PRs, in particular the nice one I saw in Lurie's SAG, just saying that `F.obj (supr U)` is the limit over the diagram of all `F.obj V` where `V` is an open subset of *some* `U i`. This version is actually much nicer to formalise, and I'm hoping we can translate over quite a lot of what we've already done about the sheaf condition to that version Co-authored-by: Scott Morrison <scott.morrison@gmail.com>