Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-02 04:41 f063221a

View on Github →

feat(topology/sheaves/skyscraper): skyscraper presheaf as a functor (#16685)

Estimated changes

Modified src/topology/sheaves/skyscraper.lean

added def skyscraper_presheaf_functor.map'

added theorem skyscraper_presheaf_functor.map'_comp

added theorem skyscraper_presheaf_functor.map'_id

added def skyscraper_presheaf_functor

added def skyscraper_sheaf_functor