Commit 2023-05-26 15:03 60dc12af

View on Github →

feat: port Topology.Sheaves.Functors (#4392)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/Functors.lean

added theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.mapCocone

added theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.map_diagram

added theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.pushforward_sheaf_of_sheaf

added def TopCat.Sheaf.pushforward

added theorem TopCat.Sheaf.pushforward_sheaf_of_sheaf