Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-05 21:07 fe37df4f

View on Github →

feat(topology/sheaves/skyscraper): stalk functor is adjoint to skyscraper functor (#16790)

Estimated changes

Modified src/topology/sheaves/skyscraper.lean

added def skyscraper_presheaf_stalk_adjunction

added def stalk_skyscraper_presheaf_adjunction_auxs.from_stalk

added theorem stalk_skyscraper_presheaf_adjunction_auxs.from_stalk_to_skyscraper

added theorem stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_from_stalk

added def stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_presheaf

added def stalk_skyscraper_sheaf_adjunction