Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-01 11:17 7295c811

View on Github →

feat(topology/sheaves/skyscraper): skyscraper presheaf is a sheaf (#16649)

depends on: #16694

Estimated changes

Modified src/topology/sheaves/skyscraper.lean

added theorem skyscraper_presheaf_eq_pushforward

added theorem skyscraper_presheaf_is_sheaf

added def skyscraper_sheaf