Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-28 03:16 7e6393f8

View on Github →

feat(topology/sheaves): the sheaf condition for functions satisfying a local predicate (#3906) Functions satisfying a local predicate form a sheaf. This sheaf has a natural map from the stalk to the original fiber, and we give conditions for this map to be injective or surjective.

Estimated changes