Commit 2023-05-27 15:27 b9fc156b

View on Github →

feat: port Topology.Sheaves.SheafCondition.UniqueGluing (#4424)

Estimated changes

Modified Mathlib.lean

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

added def TopCat.Presheaf.IsCompatible

added def TopCat.Presheaf.IsGluing

added def TopCat.Presheaf.IsSheafUniqueGluing

added theorem TopCat.Presheaf.compatible_iff_leftRes_eq_rightRes

added theorem TopCat.Presheaf.isGluing_iff_eq_res

added theorem TopCat.Presheaf.isSheafUniqueGluing_of_isSheaf_types

added theorem TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing

added theorem TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types

added theorem TopCat.Presheaf.isSheaf_of_isSheafUniqueGluing_types

added def TopCat.Presheaf.piOpensIsoSectionsFamily

added theorem TopCat.Sheaf.eq_of_locally_eq'

added theorem TopCat.Sheaf.eq_of_locally_eq

added theorem TopCat.Sheaf.eq_of_locally_eq₂

added theorem TopCat.Sheaf.existsUnique_gluing'

added theorem TopCat.Sheaf.existsUnique_gluing