Mathlib Changelog
v4
Changelog
About
Github
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