Commit 2023-05-28 08:49 e2585493

View on Github →

feat: port Topology.Sheaves.SheafOfFunctions (#4426)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/SheafOfFunctions.lean

added theorem TopCat.Presheaf.toType_isSheaf

added theorem TopCat.Presheaf.toTypes_isSheaf

added def TopCat.sheafToType

added def TopCat.sheafToTypes