Commit 2023-05-31 06:39 b940e45c

View on Github →

feat: port Topology.Sheaves.LocalPredicate (#4497)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/LocalPredicate.lean

added structure TopCat.LocalPredicate

added def TopCat.PrelocalPredicate.sheafify

added theorem TopCat.PrelocalPredicate.sheafifyOf

added structure TopCat.PrelocalPredicate

added def TopCat.continuousLocal

added def TopCat.continuousPrelocal

added def TopCat.sheafToTop

added def TopCat.stalkToFiber

added theorem TopCat.stalkToFiber_germ

added theorem TopCat.stalkToFiber_injective

added theorem TopCat.stalkToFiber_surjective

added def TopCat.subpresheafContinuousPrelocalIsoPresheafToTop

added theorem TopCat.subpresheafToTypes.isSheaf

added def TopCat.subpresheafToTypes.subtype

added def TopCat.subpresheafToTypes

added def TopCat.subsheafToTypes