mathlib

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