Commit 2023-05-21 12:23 eeb99a4f

View on Github →

feat: port Topology.Sheaves.SheafCondition.Sites (#4150)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/SheafCondition/Sites.lean

added theorem IsOpenMap.coverPreserving

added theorem OpenEmbedding.compatiblePreserving

added theorem TopCat.Opens.coverDense_iff_isBasis

added theorem TopCat.Opens.coverDense_inducedFunctor

added theorem TopCat.Presheaf.coveringOfPresieve.iSup_eq_of_mem_grothendieck

added def TopCat.Presheaf.coveringOfPresieve

added theorem TopCat.Presheaf.coveringOfPresieve_apply

added theorem TopCat.Presheaf.covering_presieve_eq_self

added theorem TopCat.Presheaf.isSheaf_of_openEmbedding

added def TopCat.Presheaf.presieveOfCovering.homOfIndex

added def TopCat.Presheaf.presieveOfCovering.indexOfHom

added theorem TopCat.Presheaf.presieveOfCovering.indexOfHom_spec

added theorem TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology

added def TopCat.Presheaf.presieveOfCovering

added def TopCat.Presheaf.presieveOfCoveringAux

added theorem TopCat.Sheaf.extend_hom_app

added theorem TopCat.Sheaf.hom_ext

added def TopCat.Sheaf.isTerminalOfEmpty

added def TopCat.Sheaf.isTerminalOfEqEmpty

added def TopCat.Sheaf.restrictHomEquivHom