Commit 2023-05-26 20:04 61bc9c0c

View on Github →

feat: port Topology.Sheaves.SheafCondition.EqualizerProducts (#4394)

Estimated changes

Modified Mathlib.lean

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

added def TopCat.Presheaf.IsSheafEqualizerProducts

added def TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIso

added def TopCat.Presheaf.SheafConditionEqualizerProducts.diagram

added def TopCat.Presheaf.SheafConditionEqualizerProducts.fork.isoOfIso

added def TopCat.Presheaf.SheafConditionEqualizerProducts.fork

added theorem TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt

added theorem TopCat.Presheaf.SheafConditionEqualizerProducts.fork_ι

added theorem TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one

added theorem TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_zero

added def TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes

added def TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.isoOfIso

added def TopCat.Presheaf.SheafConditionEqualizerProducts.piInters

added def TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.isoOfIso

added def TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens

added def TopCat.Presheaf.SheafConditionEqualizerProducts.res

added theorem TopCat.Presheaf.SheafConditionEqualizerProducts.res_π

added def TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes

added theorem TopCat.Presheaf.SheafConditionEqualizerProducts.w

added def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv

added def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso

added def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor

added def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj

added def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse

added def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj

added def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso

added def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp

added def TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitMapConeOfIsLimitSheafConditionFork

added def TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitSheafConditionForkOfIsLimitMapCone

added theorem TopCat.Presheaf.isSheaf_iff_isSheafEqualizerProducts