Commit 2023-05-27 13:11 5c0e233a

View on Github →

feat: port Topology.Sheaves.Forget (#4407)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/Forget.lean

added def TopCat.Presheaf.SheafCondition.diagramCompPreservesLimits

added def TopCat.Presheaf.SheafCondition.mapConeFork

added theorem TopCat.Presheaf.isSheaf_iff_isSheaf_comp