Mathlib v3 is deprecated. Go to Mathlib v4

Theorem skyscraper_presheaf_functor.map'_id

Modification history

2022-10-02 04:41

src/topology/sheaves/skyscraper.lean

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

Added skyscraper_presheaf_functor.map'_id View on Github →