Commit 2023-05-19 05:51 01f4692b

View on Github →

feat: port Topology.Sheaves.PresheafOfFunctions (#4092)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/PresheafOfFunctions.lean

added def TopCat.commRingYoneda

added def TopCat.continuousFunctions.map

added def TopCat.continuousFunctions.pullback

added def TopCat.continuousFunctions

added def TopCat.presheafToTop

added def TopCat.presheafToTopCommRing

added theorem TopCat.presheafToTop_obj

added def TopCat.presheafToType

added theorem TopCat.presheafToType_map

added theorem TopCat.presheafToType_obj

added def TopCat.presheafToTypes

added theorem TopCat.presheafToTypes_map

added theorem TopCat.presheafToTypes_obj