Commit 2023-05-18 18:22 d8005bc5

View on Github →

feat: port Topology.Sheaves.Sheaf (#4088)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/Sheaf.lean

added def TopCat.Presheaf.IsSheaf

added theorem TopCat.Presheaf.isSheaf_iso_iff

added theorem TopCat.Presheaf.isSheaf_of_iso

added theorem TopCat.Presheaf.isSheaf_unit

added theorem TopCat.Sheaf.comp_app

added def TopCat.Sheaf.forget

added theorem TopCat.Sheaf.id_app

added def TopCat.Sheaf