Commit 2023-05-23 15:02 5a391047

View on Github →

feat: port Topology.Sheaves.SheafCondition.OpensLeCover (#4273)

Estimated changes

Modified Mathlib.lean

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

added def TopCat.Presheaf.IsSheafOpensLeCover

added def TopCat.Presheaf.SheafCondition.OpensLeCover.homToIndex

added def TopCat.Presheaf.SheafCondition.OpensLeCover.index

added def TopCat.Presheaf.SheafCondition.OpensLeCover

added def TopCat.Presheaf.SheafCondition.opensLeCoverCocone

added def TopCat.Presheaf.generateEquivalenceOpensLe

added def TopCat.Presheaf.generateEquivalenceOpensLe_functor'

added def TopCat.Presheaf.generateEquivalenceOpensLe_inverse'

added def TopCat.Presheaf.isLimitOpensLeEquivGenerate₁

added def TopCat.Presheaf.isLimitOpensLeEquivGenerate₂

added theorem TopCat.Presheaf.isSheaf_iff_isSheafOpensLeCover

added def TopCat.Presheaf.whiskerIsoMapGenerateCocone